From f5c0396f5ff4a1357f954fccd725ca68e40bd62c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 25 Sep 2001 07:30:49 +0000
Subject: Mise en page

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

diff --git a/ANNONCE b/ANNONCE
index d581d0447f..116842347d 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -6,9 +6,9 @@ on version 7.0.
 
   - a primitive let-in construct
   - qualified names
-  - library structuration
-  - a high-level tactic language
+  - a new high-level tactic language
   - improved search facilities
+  - a new extraction algorithm managing the Type level
   - export of theories to XML for publishing and rendering purposes
   - a deep restructuration of the code (safer, simpler and more efficient)
 
@@ -26,9 +26,10 @@ on version 7.0.
   - new tactics NewDestruct, NewInduction and Assert intended to
     improve the behaviour of previous Elim and Induction, Case and
     Destruct, and Cut tactics
-  - known-bugs fixes
+  - known-bugs fixed
   - excessive memory use mainly fixed
 
+
   The Realizer/Program tactics are not available in Coq V7.1.
   The Correctness command can be used instead.
 
@@ -52,5 +53,6 @@ list of changes including sources of incompatibilities.
 and to mail Coq-Club@pauillac.inria.fr for general questions or
 remarks (moderated).
 
-  The Coq development team (in LogiCal team)
+
+      The Coq development team
 
-- 
cgit v1.2.3