1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v
new file mode 100644
index 00000000..ae212caa
--- /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 at -1. (* Error: Not convertible. *)
+  reflexivity.
+Defined.
+\ No newline at end of file