Modifs sur le langage de tactiques et pas de "ë" dans Micaela

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

1 files changed, 4 insertions, 3 deletions

diff --git a/ANNONCE b/ANNONCE
index 30eca7f390..7e33b5dcce 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -5,10 +5,11 @@ 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 (by David Delahaye)
+  - a more high-level tactic language based on a small functional core with
+    recursors and elaborated matching operators for terms and proof contexts
+    (by David Delahaye)
   - an improved Search facilities using patterns (by Yves Bertot)
-  - a "natural" syntax for real numbers (by Micaëla Mayero)
+  - a "natural" syntax for real numbers (by Micaela Mayero)
   - various bug fixes
   - a command to export theories to XML to be used with Helm's publishing
     and rendering tools (see http://www.cs.unibo.it/helm) (by Claudio