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 LaTeX
- 12.6 Coq and HTML
- 12.7 Coq and GNU Emacs
- 12.8 Module specification
- 12.9 Man pages
- Presentation of the Addendum