1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
{!indexlist}
This is Coq, a proof assistant for the Calculus of Inductive Constructions.
This document describes the implementation of Coq.
It has been automatically generated from the source of
Coq using {{:http://caml.inria.fr/}ocamldoc}.
The source files are organized in several directories ordered like that:
{ol {- Utility libraries : lib
describes the various utility libraries used in the code
of Coq.}
{- Kernel : kernel
describes the Coq kernel, which is a type checker for the Calculus
of Inductive Constructions.}
{- Library : library
describes the Coq library, which is made of two parts:
- a general mechanism to keep a trace of all operations and of
the state of the system, with backtrack capabilities;
- a global environment for the CCI, with functions to export and
import compiled modules.
}
{- Pretyping : pretyping
}
{- Front abstract syntax of terms : interp
describes the translation from Coq context-dependent
front abstract syntax of terms {v constr_expr v} to and from the
context-free, untyped, globalized form of constructions {v glob_constr v}.}
{- Parsers and printers : parsing
describes the implementation of the Coq parsers and printers.}
{- Proof engine : proofs
describes the Coq proof engine, which is also called
the ``refiner'', since it provides a way to build terms by successive
refining steps. Those steps are either primitive rules or higher-level
tactics.}
{- Tacticts : tactics
describes the Coq main tactics.}
{- Toplevel : toplevel
describes the highest modules of the Coq system.}
}
|
