diff options
| author | Arnaud Spiwack | 2015-11-06 09:18:54 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-11-11 22:14:06 +0100 |
| commit | bbfa17765599a04931efa68a5397f418e6ea5b39 (patch) | |
| tree | 983a558276920e745a65c41e864f9433f657259c | |
| parent | e82fc7cb4104d28619448bde374afde7e32f3dc2 (diff) | |
Prehistory of Coq: consistency.
Don't use abbreviated first names in sentences.
| -rw-r--r-- | dev/doc/README-V1-V5.asciidoc | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc index 43971ba553..a02f0831dc 100644 --- a/dev/doc/README-V1-V5.asciidoc +++ b/dev/doc/README-V1-V5.asciidoc @@ -194,7 +194,7 @@ Its source code was communicated to Randy Pollack on September 2nd 1988. It evolved progressively into LEGO, proof system for Luo's formalism of Extended Calculus of Constructions. -The discharge tactic was modified by G. Huet to allow for inter-dependencies +The discharge tactic was modified by Gérard Huet to allow for inter-dependencies in discharged lemmas. Christine Paulin improved the inductive definition scheme in order to accommodate predicates of any arity. @@ -227,7 +227,7 @@ yielding spectacular improvements. Thierry Coquand adapts the proof synthesis to the new representation, and simplifies pattern matching to first-order predicate calculus matching, with important performance gain. -A new representation of the universe hierarchy is then defined by G. Huet. +A new representation of the universe hierarchy is then defined by Gérard Huet. Universe levels are now implemented implicitly, through a hidden graph of abstract levels constrained with an order relation. Checking acyclicity of the graph insures well-foundedness of the ordering, |