Re: Major mode for coq

[Heime]

Sent with Proton Mail secure email.

On Monday, May 6th, 2024 at 7:08 AM, Heime <heimeborgia@protonmail.com> wrote:

> On Monday, May 6th, 2024 at 6:57 AM, Heime heimeborgia@protonmail.com wrote:
> 
> > Sent with Proton Mail secure email.
> > 
> > On Monday, May 6th, 2024 at 6:14 AM, Stefan Monnier 
> > monnier@iro.umontreal.ca wrote:
> > 
> > > > It would still be good to open a file with the highlighting before 
> > > > people
> > > > have installed "Proof General". "Proof General" could then use that mode
> > > > and do the other stuff as well. I could be more productive if I can 
> > > > change
> > > > the files without the details of "Proof General".
> > > 
> > > My crystal ball tells me you're looking for
> > > 
> > > (setq proof-splash-enable nil)
> > 
> > Would it be difficult to separate the coq-mode from the Proof General
> > IDE functionality ?
> > 
> > > - Stefan
> 
> 
> Currently I have an old machine with an old system that I cannot install
> coq in it, but I still want to view and change the files like normal .el,
> .c, and the like.

Currently the .v files load up in verilog-mode.