Dernière MAJ

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

2 files changed, 18 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index e69de29bb2..2c51e4f88a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -0,0 +1,8 @@
+English version of changes is available on
+
+  http:coq.inria.fr
+
+and
+
+  ftp://ftp.inria.fr/INRIA/coq/V7.0/Changes.ps
+
diff --git a/KNOWN-BUGS b/KNOWN-BUGS
index 5b346434cd..c36c34e915 100644
--- a/KNOWN-BUGS
+++ b/KNOWN-BUGS
@@ -1,15 +1,19 @@
   THIS IS A LIST OF KNOWN BUGS OF COQ V7.0 BETA
 
-- The syntax "Specialize num ident" is temporarily not accepted
-  outside "Tactic Definition". Syntax "Specialize ident" is OK.
-
 - Realizer and Program/Program_all are not available
 
+- Correctness is not available
+
+- Local definitions in Record/Structure are not allowed
+
+- Alias of pattern with dependent types are not supported
+
+- Tokens with both symbols and letters are not supported
+
 - No consistency check is done when requiring a module (that is, a
   module can be compiled with logical name Mycontrib.Arith.Plus but
   required with name HisContrib.Zarith.Plus).
 
-- Real numbers not subterm of a complex expression are written under a
-  form like ``4+1`` instead of ``5``.
+- The syntax "Specialize num ident" is temporarily not accepted
+  outside "Tactic Definition". Syntax "Specialize ident" is OK.
 
-- Local definitions in Record/Structure are not allowed