From 0d294b3c91e0b93cb71d3b4ef1f00ef06ad711a6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Dec 2000 18:59:08 +0000
Subject: MAJ

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

(limited to 'ANNONCE')

diff --git a/ANNONCE b/ANNONCE
index 81d2671400..30eca7f390 100644
--- a/ANNONCE
+++ b/ANNONCE
@@ -10,9 +10,9 @@ provided for users willing to experiment the new features which are:
   - 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
-    Helm's publishing and rendering tools (see http://www.cs.unibo.it/helm)
-    (by Claudio Sacerdoti Coen)
+  - 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
+    Sacerdoti Coen)
 
   Extraction and the Realizer/Program tactics are not available in Coq
 V7.0beta.
-- 
cgit v1.2.3