From d3822832501ffac6507b026e225bc2906419800e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 25 Sep 2001 11:51:53 +0000
Subject: Qqes oublis

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2068 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ANNONCE | 12 ++++++++----
 CHANGES | 21 ++++++++++++++-------
 2 files changed, 22 insertions(+), 11 deletions(-)

diff --git a/ANNONCE b/ANNONCE
index 116842347d..d311a15177 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -4,13 +4,17 @@ on version 7.0.
 
   The main features of Coq versions 7.0 and 7.1 over version 6.3.1 are
 
-  - a primitive let-in construct
+  - new primitive let-in construct
   - qualified names
-  - a new high-level tactic language
+  - new high-level tactic language
   - improved search facilities
-  - a new extraction algorithm managing the Type level
+  - new rewriting tactic for types equipped with specific equalities
+  - new tactic Field to decide equalities on commutative fields
+  - new tactic Fourier to solve linear inequalities on reals numbers
+  - new tactics for induction/case analysis in "natural" style
+  - 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)
+  - deep restructuration of the code (safer, simpler and more efficient)
 
 
   Compared to version 7.0, the new version provides with
diff --git a/CHANGES b/CHANGES
index 7c1a3aa49c..638010300d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -11,13 +11,20 @@ Notes:
 Main novelties
 ==============
 
-- new primitive let-in construct
-- long names
-- new high-level tactic language
-- improved search facilities
-- new extraction algorithm managing the Type level
-- export of theories to XML for publishing and rendering purposes
-- deep restructuration of the code (safer, simpler and more efficient)
+References are to Coq V7.1 reference manual
+
+- New primitive let-in construct (see section 1.2.8)
+- Long names (see section 2.6)
+- New high-level tactic language (see chapter 10)
+- Improved search facilities (see section 5.2)
+- New extraction algorithm managing the Type level (see chapter 17)
+- New rewriting tactic for arbitrary equalities (see chapter 19)
+- New tactic Field to decide equalities on commutative fields (see 7.11)
+- New tactic Fourier to solve linear inequalities on reals numbers (see 7.11)
+- New tactics for induction/case analysis in "natural" style (see 7.7)
+- Deep restructuration of the code (safer, simpler and more efficient)
+- Export of theories to XML for publishing and rendering purposes
+  (see http://www.cs.unibo.it/helm)
 
 
 Details of changes
-- 
cgit v1.2.3