diff options
| author | Pierre-Marie Pédrot | 2015-11-20 11:27:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-20 11:27:45 +0100 |
| commit | f01b73bd6f5a66cde730c584df6be08e06bf2042 (patch) | |
| tree | 294b074f4752fdb39f24ea4e2f55349558e9db26 /dev/doc | |
| parent | 5ccadc40d54090df5e6b61b4ecbb6083d01e5a88 (diff) | |
| parent | 574e510ba069f1747ecb1e5a17cf86c902d79d44 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'dev/doc')
| -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 |