aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/BUGS
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction/BUGS')
-rw-r--r--contrib/extraction/BUGS21
1 files changed, 0 insertions, 21 deletions
diff --git a/contrib/extraction/BUGS b/contrib/extraction/BUGS
index 3c3345da7f..8b13789179 100644
--- a/contrib/extraction/BUGS
+++ b/contrib/extraction/BUGS
@@ -1,22 +1 @@
-======================================================================
-
-Coq < Extraction Module Specif.
-Anomaly: Failure "nth". Please report.
-
-======================================================================
-
-Coq < Extraction Module Datatypes.
-
-donne le code suivant :
-
-type coq_Empty_set =
-
-let coq_Empty_set_ind =
- prop
-
-let coq_Empty_set_rec = function
-
-let coq_Empty_set_rect = function
-
-======================================================================