Stream: Coq users

Topic: coq-mode for emacs

view this post on Zulip Heime (May 05 2024 at 15:18):

In the a major mode for coq in emacs. I could only find "Proof General", but that forces the interactive display of "Proof Gereral". Rather than displaying an arbitrary coq file using coq-mode for highlighting purposes.

view this post on Zulip Pierre Courtieu (May 05 2024 at 15:57):

ProofGeneral does not start interactive coq unless you ask for it, so you can use it as a simple mode for highlighting.
It does display an image at start that you can disable with (setq proof-splash-enable nil).

Last updated: Oct 13 2024 at 01:02 UTC