aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ocamldoc/docintro
blob: 33d20fc8182b0b6cab97051bab83aae8ecd65ff8 (plain)
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.}
}