ProofGeneral release 4.5

We are happy to announce the release of Proof General version 4.5.

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.

Core maintainers e-mail:

Proof General includes these features, amongst others:

  • Script management: proof assistant state reflected in editor
  • Commands for building and replaying proofs
  • Syntax highlighting of proof scripts and prover output; hiding proofs
  • Menu for jumping to theorems in a proof script
  • Provision to easily run proof assistant on a remote host
  • Works on any system where emacs and coq are running

Summary of changes from 4.4 to 4.5:

Generic changes

  • proof-general is now a MELPA (MELPA) and NonGNU ELPA (NonGNU-devel ELPA - proof-general) Emacs package.
  • It now requires GNU Emacs 25.2 or later
  • License changed to GPL-3.0-or-later
  • Remove support for the following systems:
    Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, Isabelle, HOL98.
  • Support for Qrhl-tool (by Dominique Unruh)
  • Support for EasyCrypt (by Pierre-Yves Strub)
  • PG’s manual is continuously deployed at Documentation

Coq changes

  • Auto Compilation of Requires improved:
    • support of vos/vok compilation
    • background compilation
  • “Omit complete opaque proofs” mode for speed.
  • Automatic insertion of “Proof using” annotations.
  • Folding/unfolding hypotheses.
  • Support Ssreflect’s move=> intro style with C-c C-a TAB
  • Support Coq’s Diffs and Show Proof Diffs features.


  • New mode: opam-switch-mode (, also distributed on MELPA, allows to easily perform opam switch (and thus switch between coq versions) from within Emacs.
  • To keep PG up-to-date (Proof General), we recommend to install PG from MELPA or NonGNU-devel-ELPA and use M-x proof-upgrade-elpa-packages RET every once in a while.

The ProofGeneral Team


And for a comprehensive list of changes, see the following recap: