MAJ V7.1

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2080 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 3 deletions

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)