From c662ae83d2b7484ecdc0f4c49c3ce22c854ec587 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 21 Dec 2000 22:24:31 +0000
Subject: Re-MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1184 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ANNONCE | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/ANNONCE b/ANNONCE
index 416d0db3c2..fb6129318a 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -6,12 +6,13 @@ provided for users willing to experiment the new features which are:
   - a primitive let-in construct
   - qualified names (such as Logic.f_equal)
   - a new tactic language based on a mini functional language with higher-
-    level pattern-matching constructs on goals (contributed by David Delahaye)
-  - an improved Search facilities using patterns (contributed by Yves Bertot)
-  - a "natural" syntax for real numbers
+    level pattern-matching constructs on goals (by David Delahaye)
+  - an improved Search facilities using patterns (by Yves Bertot)
+  - a "natural" syntax for real numbers (by Micaëla Mayero)
   - various bug fixes
   - a command to export definitions, theorems and proofs to XML to be used with
-    Bologna publishing and rendering tools (see http://www.cs.unibo.it/helm)
+    Helm's publishing and rendering tools (see http://www.cs.unibo.it/helm)
+    (by Claudio Sacerdoti Coen)
 
   Extraction and the Realizer/Program tactics are not available in Coq
 V7.0beta.
@@ -29,7 +30,6 @@ and ftp://ftp.inria.fr/INRIA/coq/V7
 list of changes including sources of incompatibilities (very few).
 
 
-  The Coq development team
-  Jean-Christophe Filliâtre, Hugo Herbelin, Christine Paulin
+  Jean-Christophe Filliâtre and Hugo Herbelin
 
 
-- 
cgit v1.2.3