From 952ccff82f3f0ce050ada278dceff92fa846c01d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 22 Dec 2000 09:12:59 +0000
Subject: Création...

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

diff --git a/KNOWN-BUGS b/KNOWN-BUGS
index 126edf0d88..5b346434cd 100644
--- a/KNOWN-BUGS
+++ b/KNOWN-BUGS
@@ -1,6 +1,15 @@
-- The syntax "Specialize num ident" is temporarily not accepted outside "Tactic
-Definition". Syntax "Specialize ident" is OK.
+  THIS IS A LIST OF KNOWN BUGS OF COQ V7.0 BETA
 
-- Realizer and Program/Program_all not available
+- 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
 
+- 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``.
+
+- Local definitions in Record/Structure are not allowed
-- 
cgit v1.2.3