Re: Major mode for coq

[Philip Kaludercic]

Heime <heimeborgia@protonmail.com> writes:

> 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 ?

As mentioned in my above message, that is what `coq-use-pg' (or rather
the opposite).  So together with Stefan's suggestion, you want to set

  (setq proof-splash-enable nil
        coq-use-pg nil)

-- 
        Philip Kaludercic on peregrine