diff options
| author | Hugo Herbelin | 2015-11-15 18:51:33 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-16 13:49:36 +0100 |
| commit | 8e482fc932fa2b1893025d914d42dd17881c2fac (patch) | |
| tree | c20b545fdc59c3ce5c313fa7bdfe4a05be642f90 /dev | |
| parent | 3aeb18bf1412a27309c39713e05eca2c27706ca8 (diff) | |
Being more precise and faithful about the origin of the file reporting
about the prehistory of Coq.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/README-V1-V5 | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5 index 2ca62e3d74..ebbc057734 100644 --- a/dev/doc/README-V1-V5 +++ b/dev/doc/README-V1-V5 @@ -1,10 +1,13 @@ Notes on the prehistory of Coq -This archive contains the sources of the CONSTR ancestor of the Coq proof -assistant. CONSTR, then Coq, was designed and implemented in the Formel team, -joint between the INRIA Rocquencourt laboratory and the Ecole Normale Supérieure -of Paris, from 1984 onwards. +This document is a copy within the Coq archive of a document written +in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin +to accompany their public release of the archive of versions 1.10 to 6.2 +of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and +implemented in the Formel team, joint between the INRIA Rocquencourt +laboratory and the Ecole Normale Supérieure of Paris, from 1984 +onwards. Version 1 |