Chapter 3: The Coq library

The initial library:

it contains elementary logical notions and datatypes. It constitutes the basic state of the system directly available when running Coq;

The standard library:

general-purpose libraries containing various developments of Coq axiomatizations about sets, lists, sorting, arithmetic, etc. This library comes with the system and its modules are directly accessible through the Require command (see chapter 5);

User contributions:

Other specification and proof developments coming from the Coq users's community. These libraries are no longer distributed with the system. They are available by anonymous FTP (see section 3.3).

• 3.1 The basic library
• 3.2 The standard library
• 3.3 Users' contributions