From 6281430231c9d4ea1353372678f1eb483e32a015 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 Jun 2014 13:58:35 +0200
Subject: Fixed bug with new semantics of change.

---
 test-suite/bugs/closed/3387.v | 21 +++++++++++++++++++++
 test-suite/bugs/opened/3387.v | 19 -------------------
 2 files changed, 21 insertions(+), 19 deletions(-)
 create mode 100644 test-suite/bugs/closed/3387.v
 delete mode 100644 test-suite/bugs/opened/3387.v

diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v
new file mode 100644
index 0000000000..feff8af2a5
--- /dev/null
+++ b/test-suite/bugs/closed/3387.v
@@ -0,0 +1,21 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Record Cat := { Obj :> Type }.
+Definition set_cat := {| Obj := Type |}.
+Goal Type@{i} = Type@{j}.
+Proof.
+  (* 1 subgoals
+, subgoal 1 (ID 3)
+
+  ============================
+   Type@{Top.368} = Type@{Top.370}
+(dependent evars:) *)
+  let x := constr:(Type) in
+  let y := constr:(Obj set_cat) in
+  unify x y. (* success *)
+  let x := constr:(Type) in
+  let y := constr:(Obj set_cat) in
+  first [ unify x y | fail 2 "no unify" ];
+    change x with y. (* Error: Not convertible. *)
+  reflexivity.
+Defined.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3387.v b/test-suite/bugs/opened/3387.v
deleted file mode 100644
index 16c4e7da2f..0000000000
--- a/test-suite/bugs/opened/3387.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Set Universe Polymorphism.
-Set Printing Universes.
-Record Cat := { Obj :> Type }.
-Definition set_cat := {| Obj := Type |}.
-Goal Type@{i} = Type@{j}.
-Proof.
-  (* 1 subgoals
-, subgoal 1 (ID 3)
-
-  ============================
-   Type@{Top.368} = Type@{Top.370}
-(dependent evars:) *)
-  let x := constr:(Type) in
-  let y := constr:(Obj set_cat) in
-  unify x y. (* success *)
-  Fail let x := constr:(Type) in
-  let y := constr:(Obj set_cat) in
-  first [ unify x y | fail 2 "no unify" ];
-    change x with y. (* Error: Not convertible. *)
-- 
cgit v1.2.3