From 7cfe7d097e6f47bde2ef2dc7fbcaef340944bbd4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Jan 2002 06:20:57 +0000
Subject: Relecture

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

diff --git a/ANNONCE b/ANNONCE
index e807f493fc..fcee480f06 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -1,13 +1,16 @@
-  The Coq development team is announcing the release version 7.2 of
-Coq. This release fixes several bugs of version 7.1 and offers the following 
-novelties or improvements
+  The Coq development team is pleased to announce the release of Coq
+version 7.2. This release fixes version 7.1 known bugs and offers
+the following novelties or improvements
 
-  - Coercions allowed in Cases patterns
-  - Extended standard library
+  - Extension of standard library (sorting; trigonometric, square and square
+    root functions; basic plane geometry; finite sums; more on continuity
+    and derivability; more on min and max; tail-recursive plus and mult)
   - Extended tactic "Assert H := P" for forward reasoning
-  - New tactic "ClearBody H" to clear the body of definitions in local context
+  - Optimised extraction
+  - Coercions allowed in Cases patterns
   - New declaration "Canonical Structure id = t : I" to help resolution of
-    implicits in developments using Record/Structure (contributed by A. Saïbi)
+    implicit arguments in developments using Record/Structure
+  - New tactic "ClearBody H" to clear local definition bodies
 
   Coq V7.2 is available in several formats from http://coq.inria.fr
 and ftp://ftp.inria.fr/INRIA/coq/V7.2. We currently provide the
-- 
cgit v1.2.3