From bbfa17765599a04931efa68a5397f418e6ea5b39 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 6 Nov 2015 09:18:54 +0100 Subject: Prehistory of Coq: consistency. Don't use abbreviated first names in sentences. --- dev/doc/README-V1-V5.asciidoc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dev/doc') diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc index 43971ba55..a02f0831d 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, -- cgit v1.2.3