From bf28565aeda18a454bb750658c94a1cc56f187c7 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 26 Sep 2001 18:12:40 +0000 Subject: MAJ V7.1 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2080 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CREDITS | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'CREDITS') diff --git a/CREDITS b/CREDITS index 860aea386..7be6ff127 100644 --- a/CREDITS +++ b/CREDITS @@ -16,9 +16,9 @@ The current version V7 is a new implementation started in september 1999. J-C. Filliātre designed the architecture of the new system, a new represention of environments and wrote a new kernel for type-checking terms (LRI) - H. Herbelin introduced a new structure of terms with local -definitions and redesigned the translation from the high-level -language of Coq to the internal representation. He introduced an + H. Herbelin introduced a new structure of terms with local +definitions. He introduced ``qualified'' names, wrote a new +pattern-matching compilation algorithm and designed an algebraic structure for universes (INRIA) D. Delahaye introduced a new language for tactics (INRIA) B. Barras improved the reduction strategy for lazy evaluation (INRIA) -- cgit v1.2.3