#pragma section-numbers off #language en

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 ==

• http://coq.inria.fr/coqide/ The graphical user interface distributed with Coq.
• http://www-sop.inria.fr/lemme/pcoq/ 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.
• http://proofgeneral.inf.ed.ac.uk/ !ProofGeneral is a generic interface for proof assistants, based on the customizable text editor Emacs.
• http://tmcoq.audebaud.org/ !TmCoq integrates Coq within !TeXmacs.
• http://home.gna.org/geoproof/ !GeoProof is a dynamic geometry software, with can communicate with CoqIDE to build the formula corresponding to a geometry figure interactively.
• http://www.cs.ru.nl/~lionelm/tmEgg/ Coq plugin for !TeXmacs

== Interface for Browsing Proofs ==

• http://helm.cs.unibo.it/ 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 http://coq.inria.fr/doc.
• enscript mode for Coq http://www.cs.ru.nl/~milad/programs/enscript

== Tactics packages ==

• http://coq.inria.fr/contribs/Micromega.html: 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.

• http://www.msr-inria.inria.fr/Projects/math-components 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. (http://pauillac.inria.fr/pipermail/coq-club/2008/003486.html)"