Fix test-suite files, and move some opened to closed.

3 files changed, 0 insertions, 60 deletions

diff --git a/test-suite/bugs/opened/2310.v b/test-suite/bugs/opened/2310.v
deleted file mode 100644
index a635e6083e..0000000000
--- a/test-suite/bugs/opened/2310.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(* Dependent higher-order hole in "refine" (simplified version) *)
-
-Set Implicit Arguments.
-
-Inductive Nest t := Cons : Nest (prod t t) -> Nest t.
-
-Definition cast A x y Heq P H := @eq_rect A x P H y Heq.
-
-Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
-
-(* This used to raise an anomaly Unknown Meta in 8.2 and 8.3beta.
-   It raises a regular error in 8.3 and almost succeeds with the new
-   proof engine: there are two solutions to a unification problem
-   (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
-   leave P as subgoal or choose itself one solution *)
-
-intros. Fail refine (Cons (cast H _ y)).
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3337.v b/test-suite/bugs/opened/3337.v
deleted file mode 100644
index 06acd020a9..0000000000
--- a/test-suite/bugs/opened/3337.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Setoid.
-Goal forall x y : Set, x = y -> x = y.
-intros x y H.
-Fail rewrite_strat subterms H.
diff --git a/test-suite/bugs/opened/HoTT_coq_077.v b/test-suite/bugs/opened/HoTT_coq_077.v
deleted file mode 100644
index 68d3056619..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_077.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Set Implicit Arguments.
-
-Require Import Logic.
-
-Set Asymmetric Patterns.
-Set Record Elimination Schemes.
-Set Primitive Projections.
-
-Record prod (A B : Type) : Type :=
-  pair { fst : A; snd : B }.
-
-Print prod_rect.
-(** prod_rect =
-fun (A B : Type) (P : prod A B -> Type)
-  (f : forall (fst : A) (snd : B), P {| fst := fst; snd := snd |})
-  (p : prod A B) =>
-match p as p0 return (P p0) with
-| {| fst := x; snd := x0 |} => f x x0
-end
-     : forall (A B : Type) (P : prod A B -> Type),
-       (forall (fst : A) (snd : B), P {| fst := fst; snd := snd |}) ->
-       forall p : prod A B, P p
-
-Arguments A, B are implicit
-Argument scopes are [type_scope type_scope _ _ _]
- *)
-
-(* What I really want: *)
-Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd))
-           (p : prod A B) : P p
-  := u (fst p) (snd p).
-
-Notation typeof x := ($(let T := type of x in exact T)$) (only parsing).
-
-(* Check for eta *)
-Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect').
-
-(* Check for the recursion principle I want *)
-Fail Check eq_refl : @prod_rect = @prod_rect'.