1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
2
"http://www.w3.org/TR/REC-html40/loose.dtd">
6
<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
7
<META name="GENERATOR" content="hevea 1.07">
13
<A HREF="Reference-Manual001.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
14
<A HREF="toc.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
15
<A HREF="Reference-Manual003.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
20
<FONT COLOR=navy>Coq</FONT> is a proof assistant for higher-order logic, allowing the
21
development of computer programs consistent with their formal
22
specification. It is the result of about ten years of research of the
23
Coq project. We shall briefly survey here three main aspects: the
24
<EM>logical language</EM> in which we write our axiomatizations and
25
specifications, the <EM>proof assistant</EM> which allows the development
26
of verified mathematical proofs, and the <EM>program extractor</EM> which
27
synthesizes computer programs obeying their formal specifications,
28
written as logical assertions in the language.<BR>
30
The logical language used by <FONT COLOR=navy>Coq</FONT> is a variety of type theory,
31
called the <EM>Calculus of Inductive Constructions</EM>. Without going
32
back to Leibniz and Boole, we can date the creation of what is now
33
called mathematical logic to the work of Frege and Peano at the turn
34
of the century. The discovery of antinomies in the free use of
35
predicates or comprehension principles prompted Russell to restrict
36
predicate calculus with a stratification of <EM>types</EM>. This effort
37
culminated with <EM>Principia Mathematica</EM>, the first systematic
38
attempt at a formal foundation of mathematics. A simplification of
39
this system along the lines of simply typed lambda-calculus
40
occurred with Church's <EM>Simple Theory of Types</EM>. The
41
lambda-calculus notation, originally used for expressing
42
functionality, could also be used as an encoding of natural deduction
43
proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the
44
<EM>Automath</EM> project, the first full-scale attempt to develop and
45
mechanically verify mathematical proofs. This effort culminated with
46
Jutting's verification of Landau's <EM>Grundlagen</EM> in the 1970's.
47
Exploiting this Curry-Howard isomorphism, notable achievements in
48
proof theory saw the emergence of two type-theoretic frameworks; the
49
first one, Martin-L�f's <EM>Intuitionistic Theory of Types</EM>,
50
attempts a new foundation of mathematics on constructive principles.
51
The second one, Girard's polymorphic lambda-calculus <I>F</I><SUB><FONT SIZE=2>omega</FONT></SUB>, is
52
a very strong functional system in which we may represent higher-order
53
logic proof structures. Combining both systems in a higher-order
54
extension of the Automath languages, T. Coquand presented in 1985 the
55
first version of the <EM>Calculus of Constructions</EM>, CoC. This strong
56
logical system allowed powerful axiomatizations, but direct inductive
57
definitions were not possible, and inductive notions had to be defined
58
indirectly through functional encodings, which introduced
59
inefficiencies and awkwardness. The formalism was extended in 1989 by
60
T. Coquand and C. Paulin with primitive inductive definitions, leading
61
to the current <EM>Calculus of Inductive Constructions</EM>. This
62
extended formalism is not rigorously defined here. Rather, numerous
63
concrete examples are discussed. We refer the interested reader to
64
relevant research papers for more information about the formalism, its
65
meta-theoretic properties, and semantics. However, it should not be
66
necessary to understand this theoretical material in order to write
67
specifications. It is possible to understand the Calculus of Inductive
68
Constructions at a higher level, as a mixture of predicate calculus,
69
inductive predicate definitions presented as typed PROLOG, and
70
recursive function definitions close to the language ML.<BR>
72
Automated theorem-proving was pioneered in the 1960's by Davis and
73
Putnam in propositional calculus. A complete mechanization (in the
74
sense of a semi-decision procedure) of classical first-order logic was
75
proposed in 1965 by J.A. Robinson, with a single uniform inference
76
rule called <EM>resolution</EM>. Resolution relies on solving equations
77
in free algebras (i.e. term structures), using the <EM>unification
78
algorithm</EM>. Many refinements of resolution were studied in the
79
1970's, but few convincing implementations were realized, except of
80
course that PROLOG is in some sense issued from this effort. A less
81
ambitious approach to proof development is computer-aided
82
proof-checking. The most notable proof-checkers developed in the
83
1970's were LCF, designed by R. Milner and his colleagues at U.
84
Edinburgh, specialized in proving properties about denotational
85
semantics recursion equations, and the Boyer and Moore theorem-prover,
86
an automation of primitive recursion over inductive data types. While
87
the Boyer-Moore theorem-prover attempted to synthesize proofs by a
88
combination of automated methods, LCF constructed its proofs through
89
the programming of <EM>tactics</EM>, written in a high-level functional
90
meta-language, ML.<BR>
92
The salient feature which clearly distinguishes our proof assistant
93
from say LCF or Boyer and Moore's, is its possibility to extract
94
programs from the constructive contents of proofs. This computational
95
interpretation of proof objects, in the tradition of Bishop's
96
constructive mathematics, is based on a realizability interpretation,
97
in the sense of Kleene, due to C. Paulin. The user must just mark his
98
intention by separating in the logical statements the assertions
99
stating the existence of a computational object from the logical
100
assertions which specify its properties, but which may be considered
101
as just comments in the corresponding program. Given this information,
102
the system automatically extracts a functional term from a consistency
103
proof of its specifications. This functional term may be in turn
104
compiled into an actual computer program. This methodology of
105
extracting programs from proofs is a revolutionary paradigm for
106
software engineering. Program synthesis has long been a theme of
107
research in artificial intelligence, pioneered by R. Waldinger. The
108
Tablog system of Z. Manna and R. Waldinger allows the deductive
109
synthesis of functional programs from proofs in tableau form of their
110
specifications, written in a variety of first-order logic. Development
111
of a systematic <EM>programming logic</EM>, based on extensions of
112
Martin-L�f's type theory, was undertaken at Cornell U. by the Nuprl
113
team, headed by R. Constable. The first actual program extractor, PX,
114
was designed and implemented around 1985 by S. Hayashi from Kyoto
115
University. It allows the extraction of a LISP program from a proof
116
in a logical system inspired by the logical formalisms of S. Feferman.
117
Interest in this methodology is growing in the theoretical computer
118
science community. We can foresee the day when actual computer systems
119
used in applications will contain certified modules, automatically
120
generated from a consistency proof of their formal specifications. We
121
are however still far from being able to use this methodology in a
122
smooth interaction with the standard tools from software engineering,
123
i.e. compilers, linkers, run-time systems taking advantage of special
124
hardware, debuggers, and the like. We hope that <FONT COLOR=navy>Coq</FONT> can be of use
125
to researchers interested in experimenting with this new methodology.<BR>
127
A first implementation of CoC was started in 1984 by G. Huet and T.
128
Coquand. Its implementation language was CAML, a functional
129
programming language from the ML family designed at INRIA in
130
Rocquencourt. The core of this system was a proof-checker for CoC seen
131
as a typed lambda-calculus, called the <EM>Constructive Engine</EM>.
132
This engine was operated through a high-level notation permitting the
133
declaration of axioms and parameters, the definition of mathematical
134
types and objects, and the explicit construction of proof objects
135
encoded as lambda-terms. A section mechanism, designed and
136
implemented by G. Dowek, allowed hierarchical developments of
137
mathematical theories. This high-level language was called the
138
<EM>Mathematical Vernacular</EM>. Furthermore, an interactive
139
<EM>Theorem Prover</EM> permitted the incremental construction of proof
140
trees in a top-down manner, subgoaling recursively and backtracking
141
from dead-alleys. The theorem prover executed tactics written in CAML,
142
in the LCF fashion. A basic set of tactics was predefined, which the
143
user could extend by his own specific tactics. This system (Version
144
4.10) was released in 1989. Then, the system was extended to deal
145
with the new calculus with inductive types by C. Paulin, with
146
corresponding new tactics for proofs by induction. A new standard set
147
of tactics was streamlined, and the vernacular extended for tactics
148
execution. A package to compile programs extracted from proofs to
149
actual computer programs in CAML or some other functional language was
150
designed and implemented by B. Werner. A new user-interface, relying
151
on a CAML-X interface by D. de Rauglaudre, was designed and
152
implemented by A. Felty. It allowed operation of the theorem-prover
153
through the manipulation of windows, menus, mouse-sensitive buttons,
154
and other widgets. This system (Version 5.6) was released in 1991.<BR>
156
<FONT COLOR=navy>Coq</FONT> was ported to the new implementation Caml-light of X. Leroy and
157
D. Doligez by D. de Rauglaudre (Version 5.7) in 1992. A new version
158
of <FONT COLOR=navy>Coq</FONT> was then coordinated by C. Murthy, with new tools designed
159
by C. Parent to prove properties of ML programs (this methodology is
160
dual to program extraction) and a new user-interaction loop. This
161
system (Version 5.8) was released in May 1993. A Centaur interface
162
<FONT COLOR=navy>CTCoq</FONT> was then developed by Y. Bertot from the Croap project
163
from INRIA-Sophia-Antipolis.<BR>
165
In parallel, G. Dowek and H. Herbelin developed a new proof engine,
166
allowing the general manipulation of existential variables
167
consistently with dependent types in an experimental version of <FONT COLOR=navy>Coq</FONT>
170
The version V5.10 of <FONT COLOR=navy>Coq</FONT> is based on a generic system for
171
manipulating terms with binding operators due to Chet Murthy. A new
172
proof engine allows the parallel development of partial proofs for
173
independent subgoals. The structure of these proof trees is a mixed
174
representation of derivation trees for the Calculus of Inductive
175
Constructions with abstract syntax trees for the tactics scripts,
176
allowing the navigation in a proof at various levels of details. The
177
proof engine allows generic environment items managed in an
178
object-oriented way. This new architecture, due to C. Murthy,
179
supports several new facilities which make the system easier to extend
182
User-programmable tactics are allowed
183
<LI>It is possible to separately verify development modules, and to
184
load their compiled images without verifying them again - a quick
185
relocation process allows their fast loading
186
<LI>A generic parsing scheme allows user-definable notations, with a
187
symmetric table-driven pretty-printer
188
<LI>Syntactic definitions allow convenient abbreviations
189
<LI>A limited facility of meta-variables allows the automatic
190
synthesis of certain type expressions, allowing generic notations
191
for e.g. equality, pairing, and existential quantification.
193
In the Fall of 1994, C. Paulin-Mohring replaced the structure of
194
inductively defined types and families by a new structure, allowing
195
the mutually recursive definitions. P. Manoury implemented a
196
translation of recursive definitions into the primitive recursive
197
style imposed by the internal recursion operators, in the style of the
198
ProPre system. C. Mu�oz implemented a decision procedure for
199
intuitionistic propositional logic, based on results of R. Dyckhoff.
200
J.C. Filli�tre implemented a decision procedure for first-order
201
logic without contraction, based on results of J. Ketonen and R.
202
Weyhrauch. Finally C. Murthy implemented a library of inversion
203
tactics, relieving the user from tedious definitions of ``inversion
206
Rocquencourt, Feb. 1st 1995<BR>
210
<H2>Credits: addendum for version 6.1</H2>
212
The present version 6.1 of <FONT COLOR=navy>Coq</FONT> is based on the V5.10 architecture. It
213
was ported to the new language Objective Caml by Bruno Barras. The
214
underlying framework has slightly changed and allows more conversions
217
The new version provides powerful tools for easier developments. <BR>
219
Cristina Cornes designed an extension of the <FONT COLOR=navy>Coq</FONT> syntax to allow
220
definition of terms using a powerful pattern-matching analysis in the
221
style of ML programs.<BR>
223
Amokrane Sa�bi wrote a mechanism to simulate
224
inheritance between types families extending a proposal by Peter
225
Aczel. He also developed a mechanism to automatically compute which
226
arguments of a constant may be inferred by the system and consequently
227
do not need to be explicitly written. <BR>
229
Yann Coscoy designed a command which explains a proof term using
230
natural language. Pierre Cr�gut built a new tactic which solves
231
problems in quantifier-free Presburger Arithmetic. Both
232
functionalities have been integrated to the <FONT COLOR=navy>Coq</FONT> system by Hugo
235
Samuel Boutin designed a tactic for simplification of commutative
236
rings using a canonical set of rewriting rules and equality modulo
237
associativity and commutativity. <BR>
239
Finally the organisation of the <FONT COLOR=navy>Coq</FONT> distribution has been supervised
240
by Jean-Christophe Filli�tre with the help of Judica�l Courant
241
and Bruno Barras.<BR>
243
Lyon, Nov. 18th 1996<BR>
247
<H2>Credits: addendum for version 6.2</H2>
249
In version 6.2 of <FONT COLOR=navy>Coq</FONT>, the parsing is done using camlp4, a
250
preprocessor and pretty-printer for CAML designed by Daniel de
251
Rauglaudre at INRIA. Daniel de Rauglaudre made the first adaptation
252
of <FONT COLOR=navy>Coq</FONT> for camlp4, this work was continued by Bruno Barras who also
253
changed the structure of <FONT COLOR=navy>Coq</FONT> abstract syntax trees and the primitives
254
to manipulate them. The result of
255
these changes is a faster parsing procedure with greatly improved
256
syntax-error messages. The user-interface to introduce grammar or
257
pretty-printing rules has also changed.<BR>
259
Eduardo Gim�nez redesigned the internal
260
tactic libraries, giving uniform names
261
to Caml functions corresponding to <FONT COLOR=navy>Coq</FONT> tactic names. <BR>
263
Bruno Barras wrote new more efficient reductions functions.<BR>
265
Hugo Herbelin introduced more uniform notations in the <FONT COLOR=navy>Coq</FONT>
266
specification language: the definitions by fixpoints and
267
pattern-matching have a more readable syntax. Patrick Loiseleur
268
introduced user-friendly notations for arithmetic expressions.<BR>
270
New tactics were introduced: Eduardo Gim�nez improved a mechanism to
271
introduce macros for tactics, and designed special tactics for
272
(co)inductive definitions; Patrick Loiseleur designed a tactic to
273
simplify polynomial expressions in an arbitrary commutative ring which
274
generalizes the previous tactic implemented by Samuel Boutin.
275
Jean-Christophe Filli�tre introduced a tactic for refining a goal,
276
using a proof term with holes as a proof scheme.<BR>
278
David Delahaye designed the <FONT COLOR=purple>SearchIsos</FONT> tool to search an
279
object in the library given its type (up to isomorphism).<BR>
281
Henri Laulh�re produced the <FONT COLOR=navy>Coq</FONT> distribution for the Windows environment. <BR>
283
Finally, Hugo Herbelin was the main coordinator of the <FONT COLOR=navy>Coq</FONT>
284
documentation with principal contributions by Bruno Barras, David Delahaye,
285
Jean-Christophe Filli�tre, Eduardo
286
Gim�nez, Hugo Herbelin and Patrick Loiseleur. <BR>
288
Orsay, May 4th 1998<BR>
292
<H2>Credits: addendum for version 6.3</H2>
293
The main changes in version V6.3 was the introduction of a few new tactics
294
and the extension of the guard condition for fixpoint definitions.<BR>
296
B. Barras extended the unification algorithm to complete partial terms
297
and solved various tricky bugs related to universes.<BR>
298
D. Delahaye developed the <TT>AutoRewrite</TT> tactic. He also designed the new
299
behavior of <TT>Intro</TT> and provided the tacticals <TT>First</TT> and
301
J.-C. Filli�tre developed the <TT>Correctness</TT> tactic.<BR>
302
E. Gim�nez extended the guard condition in fixpoints.<BR>
303
H. Herbelin designed the new syntax for definitions and extended the
304
<TT>Induction</TT> tactic.<BR>
305
P. Loiseleur developed the <TT>Quote</TT> tactic and
306
the new design of the <TT>Auto</TT>
307
tactic, he also introduced the index of
308
errors in the documentation.<BR>
309
C. Paulin wrote the <TT>Focus</TT> command and introduced
310
the reduction functions in definitions, this last feature
311
was proposed by J.-F. Monin from CNET Lannion. <BR>
317
<H2>Credits: versions 7</H2>
318
The version V7 is a new implementation started in September 1999 by
319
Jean-Christophe Filli�tre. This is a major revision with respect to
320
the internal architecture of the system. The <FONT COLOR=navy>Coq</FONT> version 7.0 was
321
distributed in March 2001, version 7.1 in September 2001, version
322
7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in
325
Jean-Christophe Filli�tre designed the architecture of the new system, he
326
introduced a new representation for environments and wrote a new kernel
327
for type-checking terms. His approach was to use functional
328
data-structures in order to get more sharing, to prepare the addition
329
of modules and also to get closer to a certified kernel.<BR>
331
Hugo Herbelin introduced a new structure of terms with local
332
definitions. He introduced ``qualified'' names, wrote a new
333
pattern-matching compilation algorithm and designed a more compact
334
algorithm for checking the logical consistency of universes. He
335
contributed to the simplification of <FONT COLOR=navy>Coq</FONT> internal structures and the
336
optimisation of the system. He added basic tactics for forward
337
reasoning and coercions in patterns.<BR>
339
David Delahaye introduced a new language for tactics. General tactics
340
using pattern-matching on goals and context can directly be written
341
from the <FONT COLOR=navy>Coq</FONT> toplevel. He also provided primitives for the design
342
of user-defined tactics in <FONT COLOR=navy>Caml</FONT>.<BR>
344
Micaela Mayero contributed the library on real numbers.
345
Olivier Desmettre extended this library with axiomatic
346
trigonometric functions, square, square roots, finite sums, Chasles
347
property and basic plane geometry.<BR>
349
Jean-Christophe Filli�tre and Pierre Letouzey redesigned a new
350
extraction procedure from <FONT COLOR=navy>Coq</FONT> terms to <FONT COLOR=navy>Caml</FONT> or
351
<FONT COLOR=navy>Haskell</FONT> programs. This new
352
extraction procedure, unlike the one implemented in previous version
353
of <FONT COLOR=navy>Coq</FONT> is able to handle all terms in the Calculus of Inductive
354
Constructions, even involving universes and strong elimination. P.
355
Letouzey adapted user contributions to extract ML programs when it was
357
Jean-Christophe Filli�tre wrote <CODE>coqdoc</CODE>, a documentation
358
tool for <FONT COLOR=navy>Coq</FONT> libraries usable from version 7.2.<BR>
360
Bruno Barras improved the reduction algorithms efficiency and
361
the confidence level in the correctness of <FONT COLOR=navy>Coq</FONT> critical type-checking
364
Yves Bertot designed the <TT>SearchPattern</TT> and
365
<TT>SearchRewrite</TT> tools and the support for the <FONT COLOR=navy>pcoq</FONT> interface
366
(<TT>http://www-sop.inria.fr/lemme/pcoq/</TT>).<BR>
368
Micaela Mayero and David Delahaye introduced <TT>Field</TT>, a decision tactic for commutative fields.<BR>
370
Christine Paulin changed the elimination rules for empty and singleton
371
propositional inductive types.<BR>
373
Lo�c Pottier developed <TT>Fourier</TT>, a tactic solving linear inequalities on real numbers.<BR>
375
Pierre Cr�gut developed a new version based on reflexion of the <TT>Omega</TT>
378
Claudio Sacerdoti Coen designed an XML output for the <FONT COLOR=navy>Coq</FONT>
379
modules to be used in the Hypertextual Electronic Library of
380
Mathematics (HELM cf <TT>http://www.cs.unibo.it/helm</TT>).<BR>
382
A library for efficient representation of finite maps using binary trees
383
contributed by Jean Goubault was integrated in the basic theories.<BR>
385
Jacek Chrzaszcz designed and implemented the module system of
386
<FONT COLOR=navy>Coq</FONT> whose foundations are in Judica�l Courant's PhD thesis.<BR>
392
The development was coordinated by C. Paulin.<BR>
394
Many discussions within the D�mons team and the LogiCal project
395
influenced significantly the design of <FONT COLOR=navy>Coq</FONT> especially with
396
J. Courant, P. Courtieu, J. Duprat, J. Goubault, A. Miquel,
397
C. March�, B. Monate and B. Werner.<BR>
399
Intensive users suggested improvements of the system :
400
Y. Bertot, L. Pottier, L. Th�ry , P. Zimmerman from INRIA,
401
C. Alvarado, P. Cr�gut, J.-F. Monin from France Telecom R & D.
404
Hugo Herbelin & Christine Paulin
407
<H2>Credits: version 8.0</H2>
408
<FONT COLOR=navy>Coq</FONT> version 8 is a major revision of the <FONT COLOR=navy>Coq</FONT> proof assistant.
409
First, the underlying logic is slightly different. The so-called <EM>impredicativity</EM> of the sort <TT>Set</TT> has been dropped. The main
410
reason is that it is inconsistent with the principle of description
411
which is quite a useful principle for formalizing mathematics within classical logic. Moreover, even in an constructive
412
setting, the impredicativity of <TT>Set</TT> does not add so much in
413
practice and is even subject of criticism from a large part of the
414
intuitionistic mathematician community. Nevertheless, the
415
impredicativity of <TT>Set</TT> remains optional for users interested in
416
investigating mathematical developments which rely on it.<BR>
418
Secondly, the concrete syntax of terms has been completely
419
revised. The main motivations were
421
a more uniform, purified style: all constructions are now lowercase,
422
with a functional programming perfume (e.g. abstraction is now
423
written <TT>fun</TT>), and more directly accessible to the novice
424
(e.g. dependent product is now written <TT>forall</TT> and allows
425
omission of types). Also, parentheses and are no longer mandatory
426
for function application.
427
<LI>extensibility: some standard notations (e.g. ``<'' and ``>'') were
428
incompatible with the previous syntax. Now all standard arithmetic
429
notations (=, +, *, /, <, <=, ... and more) are directly part of the
432
Together with the revision of the concrete syntax, a new mechanism of
433
<EM>interpretation scopes</EM> permits to reuse the same symbols
434
(typically +, -, *, /, <, <=) in various mathematical theories without
435
any ambiguities for <FONT COLOR=navy>Coq</FONT>, leading to a largely improved readability of
436
<FONT COLOR=navy>Coq</FONT> scripts. New commands to easily add new symbols are also
439
Coming with the new syntax of terms, a slight reform of the tactic
440
language and of the language of commands has been carried out. The
441
purpose here is a better uniformity making the tactics and commands
442
easier to use and to remember.<BR>
444
Thirdly, a restructuration and uniformisation of the standard library
445
of <FONT COLOR=navy>Coq</FONT> has been performed. There is now just one Leibniz' equality
446
usable for all the different kinds of <FONT COLOR=navy>Coq</FONT> objects. Also, the set of
447
real numbers now lies at the same level as the sets of natural and
448
integer numbers. Finally, the names of the standard properties of
449
numbers now follow a standard pattern and the symbolic
450
notations for the standard definitions as well.<BR>
452
The fourth point is the release of <FONT COLOR=navy>CoqIDE</FONT>, a new graphical
453
gtk2-based interface fully integrated to <FONT COLOR=navy>Coq</FONT>. Close in style from
454
the Proof General Emacs interface, it is faster and its integration
455
with <FONT COLOR=navy>Coq</FONT> makes interactive developments more friendly. All
456
mathematical Unicode symbols are usable within <FONT COLOR=navy>CoqIDE</FONT>.<BR>
458
Finally, the module system of <FONT COLOR=navy>Coq</FONT> completes the picture of <FONT COLOR=navy>Coq</FONT>
459
version 8.0. Though released with an experimental status in the previous
460
version 7.4, it should be considered as a salient feature of the new
463
Besides, <FONT COLOR=navy>Coq</FONT> comes with its load of novelties and improvements: new
464
or improved tactics (including a new tactic for solving first-order
465
statements), new management commands, extended libraries.<BR>
471
Bruno Barras and Hugo Herbelin have been the main contributors of the
472
reflexion and the implementation of the new syntax. The smart
473
automatic translator from old to new syntax released with <FONT COLOR=navy>Coq</FONT> is also
474
their work with contributions by Olivier Desmettre.<BR>
476
Hugo Herbelin is the main designer and implementor of the notion of
477
interpretation scopes and of the commands for easily adding new notations.<BR>
479
Hugo Herbelin is the main implementor of the restructuration of the
480
standard library.<BR>
482
Pierre Corbineau is the main designer and implementor of the new
483
tactic for solving first-order statements in presence of inductive
484
types. He is also the maintainer of the non-domain specific automation
487
Benjamin Monate is the developer of the <FONT COLOR=navy>CoqIDE</FONT> graphical
488
interface with contributions by Jean-Christophe Filli�tre, Pierre
489
Letouzey and Claude March�.<BR>
491
Claude March� coordinated the edition of the Reference Manual for
492
<FONT COLOR=navy>Coq</FONT> V8.0.<BR>
494
Pierre Letouzey and Jacek Chrzaszcz respectively maintained the
495
extraction tool and module system of <FONT COLOR=navy>Coq</FONT>.<BR>
497
Jean-Christophe Filli�tre, Pierre Letouzey, Hugo Herbelin and
498
contributors from Sophia-Antipolis and Nijmegen participated to the
499
extension of the library.<BR>
501
Hugo Herbelin and Christine Paulin coordinated the development which
502
was under the responsability of Christine Paulin.<BR>
504
Palaiseau & Orsay, Apr. 2004<BR>
505
Hugo Herbelin & Christine Paulin
509
<A HREF="Reference-Manual001.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
510
<A HREF="toc.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
511
<A HREF="Reference-Manual003.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
added
removed
manual/Reference-Manual002.html
