proof-general

Homepage: https://proofgeneral.github.io

Author: (see the AUTHORS file distributed along the sources)

Updated: 2024-Nov-26

Summary

A generic Emacs interface for proof assistants

Commentary

Proof General is a generic Emacs interface for proof assistants
(also known as interactive theorem provers).

It is supplied ready to use for the proof assistants Coq,
EasyCrypt, qrhl-tool, and PhoX.

See https://proofgeneral.github.io/ for installation instructions
and online documentation.  Or browse the accompanying info manual:
(info-display-manual "ProofGeneral")

Regarding the Coq proof assistant, you may be interested in the
company-coq extension of ProofGeneral (also available in MELPA).

Dependencies

• cl-lib
• comint
• compile
• completion
• custom
• diff-mode
• easymenu
• elp
• ert
• etags
• font-lock
• fontset
• newcomment
• outline
• quail
• reporter
• ring
• seq
• smie
• subr-x
• tool-bar
• whitespace
• xml

Reverse dependencies

• alectryon
• syntactic-close