Chapter 12: Utilities
The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation.
12.1 Building a toplevel extended with user tactics
12.2 Modules dependencies
12.3 Creating a
Makefile
for
Coq
modules
12.4
Coq_SearchIsos
: information retrieval in a
Coq
proofs library
12.5
Coq
and L
A
T
E
X
12.6
Coq
and HTML
12.7
Coq
and
GNU Emacs
12.8 Module specification
12.9 Man pages
Presentation of the Addendum
