This repo is the new home of Proof General
Proof General is a generic Emacs mode for proof assistants. It can be instantiated for the proof assistant of your choice, and is supplied ready-customized for Coq, PhoX, EasyCrypt, Qrhl-tool.
Proof General includes these features, amongst others:
move=>
intro style with C-c C-a TAB
Diffs
and Show Proof Diffs
features.opam-switch-mode
(https://github.com/ProofGeneral/opam-switch-mode), also distributed on MELPA, allows to easily perform opam switch
(and thus switch between coq versions) from within emacs.M-x proof-upgrade-elpa-packages RET
every once in a while.Proof General 4.4