Proof General is a major mode to turn Emacs into an interactive proof assistant to write formal mathematical proofs using a variety of theorem provers. It works with either XEmacs or GNU Emacs. . This package provides the Proof General support for the Coq theorem prover which is available as another package. The package is however not required to just edit Coq files.