From f907cc977bb80e3654174de03aeaed2cb4aa4a7e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 15 Apr 2008 16:35:54 +0000
Subject: Mises à jour bugs, CHANGES, code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10801 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/opened/shouldnotfail/1774.v | 18 -------------
 test-suite/bugs/opened/shouldnotfail/1775.v | 39 -----------------------------
 2 files changed, 57 deletions(-)
 delete mode 100644 test-suite/bugs/opened/shouldnotfail/1774.v
 delete mode 100644 test-suite/bugs/opened/shouldnotfail/1775.v

(limited to 'test-suite/bugs/opened/shouldnotfail')

diff --git a/test-suite/bugs/opened/shouldnotfail/1774.v b/test-suite/bugs/opened/shouldnotfail/1774.v
deleted file mode 100644
index 4c24b481bd..0000000000
--- a/test-suite/bugs/opened/shouldnotfail/1774.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop).
-Axiom plImp : forall k P Q,
-  pl P Q k -> forall (P':nat -> Prop),
-    (forall k', P k' -> P' k') -> forall (Q':nat -> Prop),
-      (forall k', Q k' -> Q' k') ->
-      pl P' Q' k.
-
-Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
-  fun k' => exists k, P k k'.
-
-Goal forall k (A:nat -> nat -> Prop) (B:nat -> Prop),
-  pl (nexists A) B k.
-intros.
-eapply plImp.
-2:intros m' M'; econstructor; apply M'.
-2:intros m' M'; apply M'.
-simpl.
-Admitted.
diff --git a/test-suite/bugs/opened/shouldnotfail/1775.v b/test-suite/bugs/opened/shouldnotfail/1775.v
deleted file mode 100644
index dab4120b96..0000000000
--- a/test-suite/bugs/opened/shouldnotfail/1775.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Axiom pair : nat -> nat -> nat -> Prop.
-Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop).
-Axiom plImp : forall k P Q,
-  pl P Q k -> forall (P':nat -> Prop),
-    (forall k', P k' -> P' k') -> forall (Q':nat -> Prop),
-      (forall k', Q k' -> Q' k') ->
-      pl P' Q' k.
-
-Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
-  fun k' => exists k, P k k'.
-
-Goal forall s k k' m,
-  (pl k' (nexists (fun w => (nexists (fun b => pl (pair w w)
-    (pl (pair s b)
-    (nexists (fun w0 => (nexists (fun a => pl (pair b w0)
-      (nexists (fun w1 => (nexists (fun c => pl 
-        (pair a w1) (pl (pair a c) k))))))))))))))) m.
-intros.
-eapply plImp; [ | eauto | intros ].
-2:econstructor.
-2:econstructor.
-2:eapply plImp; [ | eauto | intros ].
-3:eapply plImp; [ | eauto | intros ].
-4:econstructor.
-4:econstructor.
-4:eapply plImp; [ | eauto | intros ].
-5:econstructor.
-5:econstructor.
-5:eauto.
-4:eauto.
-3:eauto.
-2:eauto.
-
-assert (X := 1).
-clear X.   (* very slow! *)
-
-simpl.  (* exception Not_found *)
-
-Admitted.
-- 
cgit v1.2.3