1 files changed, 0 insertions, 33 deletions
diff --git a/test-suite/bugs/opened/3657.v b/test-suite/bugs/opened/3657.v
deleted file mode 100644
index 6faec076..00000000
--- a/test-suite/bugs/opened/3657.v
+++ /dev/null
@@ -1,33 +0,0 @@
-(* Set Primitive Projections. *)
-Class foo {A} {a : A} := { bar := a; baz : bar = bar }.
-Arguments bar {_} _ {_}.
-Instance: forall A a, @foo A a.
-intros; constructor.
-abstract reflexivity.
-Defined.
-Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat.
-Proof.
-  Check (bar Set).
-  Check (bar (fun _ : Set => Set)).
-  Fail change (bar (fun _ : Set => Set)) with (bar Set). (* Error: Conversion test raised an anomaly *)
-
-Abort.
-
-
-Module A.
-Universes i j.
-Constraint i < j.
-Variable  foo : Type@{i}.
-Goal Type@{i}.
-  Fail let t := constr:(Type@{j}) in
-  change Type with t.
-Abort.
-
-Goal Type@{j}.
-  Fail let t := constr:(Type@{i}) in
-  change Type with t.
-  let t := constr:(Type@{i}) in
-  change t. exact foo.
-Defined.
-
-End A.