A library of Coq definitions, theorems, and tactics.
Coq Makefile
Pull request Compare This branch is 4 commits ahead, 66 commits behind v8.5.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.



A collection of theories and plugins that may be useful in other Coq developments.


  • Use modules for controlling namespaces.
  • Avoid functors in favor of type classes since type classes are more flexible b/c they are first-class.
  • Notations should be hidden by modules that are explicitly opened.
    • This avoids clashes between precedence.
    • TB: Actually, this does not completely avoid clashes, if we have to open two modules at the same time (for instance, I often need to open Equality, to get dependent destruction, which conflicts with the rest of my development)
    • TB: I like the idea of having to prefix operations by the name of the module (e.g., DList.fold, DList.map, DList.T), and yet to benefit from the support of notations, without opening this module. I implement that by having a module DList that contains the operations, inside the file DList. The notations live in the file DList, and I do Require Import DList everywhere...
  • Avoid the use of the 'core' hint database.
  • Avoid the use of dependent functions, e.g. dependendent decidable equality, in favor of their boolen counter-parts. Use type-classes to expose the proofs. -

File Structure

  • plugins/
    • Base directory to the provided plugins
  • theories/
    • Base directory to the provided theories

Install from OPAM

Make sure you added the Coq repository:

opam repo add coq-released https://coq.inria.fr/opam/released

and run:

opam install coq-ext-lib