Re: Major mode for coq

[Philip Kaludercic <philipk@posteo.net>]

Heime <heimeborgia@protonmail.com> writes:

> Sent with Proton Mail secure email.
>
> On Monday, May 6th, 2024 at 1:51 AM, Stefan Monnier via Users list for
> the GNU Emacs text editor <help-gnu-emacs@gnu.org> wrote:
>
>> > Is there any major mode for coq formal proof management system files ?
>> 
>> 
>> I don't know what you mean by "system files", but there's a coq-mode as
>> part of Proof-General (available in NonGNU ELPA). - Stefan
>
> Right.  But I was hoping to see something that we are all familiar with.
> Open the file with a coq-mode without the interface of "Proof General".
> Just see some highlighting and some tools for the file type, as one gets 
> with elisp, c, and fortran.  Currently the language highlighting only
> gets activated as a proof general feature.  It goes much beyond just showing
> the contents of the file.

Proof-general includes a coq-mode, and there is a user option
`coq-use-pg' that can disable integration with Proof General (but
usually you don't want that, since having the interaction with the Coq
system is what makes working with Coq in Emacs interesting).

-- 
	Philip Kaludercic on icterid