From 65d027ba5ffcec61e66b1a047b135bea2f281c44 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 10 Feb 2009 14:58:38 +0000
Subject: removed prehistoric files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11903 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 KNOWN-BUGS | 20 --------------------
 1 file changed, 20 deletions(-)
 delete mode 100644 KNOWN-BUGS

(limited to 'KNOWN-BUGS')

diff --git a/KNOWN-BUGS b/KNOWN-BUGS
deleted file mode 100644
index 774d181cf9..0000000000
--- a/KNOWN-BUGS
+++ /dev/null
@@ -1,20 +0,0 @@
-  THIS IS A LIST OF KNOWN BUGS OF COQ V7.0
-
-- Realizer and Program/Program_all are 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).
-
-- The syntax "Specialize num ident" is temporarily not accepted
-  outside "Tactic Definition". Syntax "Specialize ident" is OK.
-
-- New Induction fails for mutual inductive elimination
-
-- Elim fails with eliminators not imported
\ No newline at end of file
-- 
cgit v1.2.3