Imported Upstream version 8.5~beta1+dfsg

1 files changed, 0 insertions, 39 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1775.v b/test-suite/bugs/closed/shouldsucceed/1775.v
deleted file mode 100644
index 932949a3..00000000
--- a/test-suite/bugs/closed/shouldsucceed/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.