*** empty log message ***

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

1 files changed, 36 insertions, 0 deletions

diff --git a/ANNONCE b/ANNONCE
new file mode 100644
index 000000000..215207679
--- /dev/null
+++ b/ANNONCE
@@ -0,0 +1,36 @@
+
+  The LogiCal team (ex-Coq team) is releasing a new version of Coq.
+Its name is V7.0beta. This new version is still in debugging phase
+and is 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 (contributed by David Delahaye)
+  - a new decision tactic for the real field (contributed by David Delahaye
+    and Micaëla Mayero)
+  - an improved Search facilities using patterns (contributed by Yves Bertot)
+  - various bug fixes
+  - new user contributions on ...
+  - a module to export definitions, theorems and proofs to XML to be
+    used with Bologna rendering tools (see http://www.cs.unibo.it/helm)
+
+  Extraction and the Realizer/Program tactics are not available in Coq V7.0. 
+
+  The internals of Coq have changed a lot. For the user, this shows
+through new and located error messages, improved efficiency, safer
+proof-checker. This justifies the new major version number 7.
+
+  However, the internals of Coq will continue to change significantly
+in the next months and we recommend tactic developers to take contact
+with us for adapting their code.
+
+  Coq V7.0beta is available as a source package from http://coq.inria.fr
+and ftp://ftp.inria.fr/INRIA/coq/V7
+
+  Please refer to the document CHANGES in the archive for a full list
+of changes including sources of incompatibilities (very few).
+
+  Jean-Christophe Filliâtre and Hugo Herbelin
+