Configuration of Proof General - coq/coq GitHub Wiki

Configuration with vanilla emacs

Configuration with spacemacs

A coq layer is available in the develop branch of spacemacs (documentation). If you are tracking the develop branch, it is enough to add coq to the existing dotspacemacs-configuration-layers list in your ~/.spacemacs (SPC f e d) and reload the configuration (SPC f e R).

Configuration with doom-emacs

Other informations

Old pages on Proof General (possibly deprecated)

• How do I change the Proof General Error Color?
• I'm using Proof General. Where did my proof state go?

Related incomplete page: shortcuts to develop with emacs