From 7012d65f71752a89cded69d6c2e7045f3a7cadde Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 27 Feb 2015 13:29:11 +0100
Subject: Moving tests for #2456 and #3593 to "opened" until they're fixed.

---
 test-suite/bugs/closed/2456.v | 53 -------------------------------------------
 test-suite/bugs/closed/3593.v | 10 --------
 2 files changed, 63 deletions(-)
 delete mode 100644 test-suite/bugs/closed/2456.v
 delete mode 100644 test-suite/bugs/closed/3593.v

(limited to 'test-suite/bugs/closed')

diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/closed/2456.v
deleted file mode 100644
index 56f046c4d7..0000000000
--- a/test-suite/bugs/closed/2456.v
+++ /dev/null
@@ -1,53 +0,0 @@
-
-Require Import Equality.
-
-Parameter Patch : nat -> nat -> Set.
-
-Inductive Catch (from to : nat) : Type
-    := MkCatch : forall (p : Patch from to),
-                 Catch from to.
-Implicit Arguments MkCatch [from to].
-
-Inductive CatchCommute5
-        : forall {from mid1 mid2 to : nat},
-          Catch from mid1
-       -> Catch mid1 to
-       -> Catch from mid2
-       -> Catch mid2 to
-       -> Prop
-     := MkCatchCommute5 :
-           forall {from mid1 mid2 to : nat}
-                  (p : Patch from mid1)
-                  (q : Patch mid1 to)
-                  (q' : Patch from mid2)
-                  (p' : Patch mid2 to),
-           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
-
-Inductive CatchCommute {from mid1 mid2 to : nat}
-                       (p : Catch from mid1)
-                       (q : Catch mid1 to)
-                       (q' : Catch from mid2)
-                       (p' : Catch mid2 to)
-                     : Prop
-    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
-                         CatchCommute p q q' p'.
-Notation "<< p , q >> <~> << q' , p' >>"
-    := (CatchCommute p q q' p')
-    (at level 60, no associativity).
-
-Lemma CatchCommuteUnique2 :
-      forall {from mid mid' to : nat}
-             {p   : Catch from mid}  {q   : Catch mid  to}
-             {q'  : Catch from mid'} {p'  : Catch mid' to}
-             {q'' : Catch from mid'} {p'' : Catch mid' to}
-             (commute1 : <<p, q>> <~> <<q', p'>>)
-             (commute2 : <<p, q>> <~> <<q'', p''>>),
-      (p' = p'') /\ (q' = q'').
-Proof with auto.
-intros.
-set (X := commute2).
-dependent destruction commute1;
-dependent destruction catchCommuteDetails;
-dependent destruction commute2;
-dependent destruction catchCommuteDetails generalizing X.
-Admitted.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3593.v b/test-suite/bugs/closed/3593.v
deleted file mode 100644
index 25f9db6b28..0000000000
--- a/test-suite/bugs/closed/3593.v
+++ /dev/null
@@ -1,10 +0,0 @@
-Set Universe Polymorphism.
-Set Printing All.
-Set Implicit Arguments.
-Record prod A B := pair { fst : A ; snd : B }.
-Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
-simpl; intros.
-  constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
-  Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). 
-  reflexivity.
-Qed.
-- 
cgit v1.2.3