Some of the tools listed here are part of bigger projects that support other proof assistants/theorem provers. Another list of Coq-related tools can be found at http://coq.inria.fr/tools1-eng.html.
Interface for Editing Proofs
- The graphical user interface distributed with Coq.
- A graphical user interface for Coq. The environment provides ways to edit structurally formulas and commands, new notations can easily be added. It allows proof by pointing.
ProofGeneral is a generic interface for proof assistants, based on the customizable text editor Emacs.
TmCoq integrates Coq within TeXmacs.
GeoProof is a dynamic geometry software, with can communicate with CoqIDE to build the formula corresponding to a geometry figure interactively.
Papuq is patched version of CoqIde with teaching oriented features.
Coq plugin for TeXmacs
Interface for Browsing Proofs
Helm is a browsable and searchable (using the Whelp tool) repository of formal mathematics (includes the Coq User Contributions).
Presenting Proofs
coqdoc exports vernacular file to TeX or HTML. It is part of the Coq distribution and documented in the Reference Manual.
enscript mode for Coq http://www.cs.ru.nl/~milad/programs/enscript
Tactics packages
Micromega: solves linear (Fourier-Motzkin) and non linear (Sum-of-Square's algorithm) systems of polynomial inequations; also provides a (partial) replacement for the Coq's omega tactic.
Ssreflect facilitates proof by small scale reflection, "a style of proof that ... provide[s] effective automation for many small, clerical proof steps. This is often accomplished by restating ("reflecting") problems in a more concrete form ... For example, in the Ssreflect library arithmetic comparison is not an abstract predicate, but a function computing a boolean. (source)"
Packaging extracted code
Z_interface An approach for deriving directly standalone programs from extracted code.