Books

• Coq's reference manual
  • The full manual: Coq's reference manual
  • An interesting page: Detailed tactic examples
• Logical foundations
  • The full book: Logical foundations
  • An interesting page: Induction.v
• A chapter from CPDT:
  • proof-by-reflection: reST sources, webpage, untangled
• A chapter from FRAP:
  • interpreters: reST sources, webpage, untangled

Libraries

• Coq's standard library
  • The library: Coq's standard library
  • An interesting page: List.v
• Flocq
  • The library: Flocq
  • An interesting page: Ulp.v

Snippets

These examples are all shown in the paper:

• Appendices:
  • life.v (MathJax): source, webpage
  • rbt.v (MathJax): source, webpage
  • nsum-gauss.rst (MathJax): source, webpage
  • Qle-pairwise.rst (MathJax): source, webpage
  • udiv.v (Pretty-printing): source, webpage
  • rss.v (Plain-HTML output): source, webpage
• Short Coq files:
  • induction.v: source, webpage
  • folded.v: source, webpage
  • classical.v: source, webpage
  • notations.v: source, webpage
  • fails.v: source, webpage
• A short reST file:
  • doc.rst: source, webpage
• A longer Coq file to test the various display modes:
  • ide.v: source, webpage
• A short CoqDoc file:
  • functions.coqdoc.v: source, webpage