aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--KNOWN-BUGS4
1 files changed, 1 insertions, 3 deletions
diff --git a/KNOWN-BUGS b/KNOWN-BUGS
index 73f4430bcc..774d181cf9 100644
--- a/KNOWN-BUGS
+++ b/KNOWN-BUGS
@@ -1,9 +1,7 @@
- THIS IS A LIST OF KNOWN BUGS OF COQ V7.0 BETA
+ THIS IS A LIST OF KNOWN BUGS OF COQ V7.0
- 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