Fix #7421: constr_eq ignores universe constraints.

The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.

1 files changed, 39 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/7421.v b/test-suite/bugs/closed/7421.v
new file mode 100644
index 000000000..afcdd35fc
--- /dev/null
+++ b/test-suite/bugs/closed/7421.v
@@ -0,0 +1,39 @@
+
+
+Universe i j.
+
+Goal False.
+Proof.
+  Check Type@{i} : Type@{j}.
+  Fail constr_eq_strict Type@{i} Type@{j}.
+  assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *)
+  Fail constr_eq_strict Type@{i} Type@{j}.
+
+  constr_eq Type@{i} Type@{j}. (* <- i=j is retained *)
+  constr_eq_strict Type@{i} Type@{j}.
+  Fail Check Type@{i} : Type@{j}.
+
+  Fail constr_eq Prop Set.
+  Fail constr_eq Prop Type.
+
+  Fail constr_eq_strict Type Type.
+  constr_eq Type Type.
+
+  constr_eq_strict Set Set.
+  constr_eq Set Set.
+  constr_eq Prop Prop.
+
+  let x := constr:(Type) in constr_eq_strict x x.
+  let x := constr:(Type) in constr_eq x x.
+
+  Fail lazymatch type of prod with
+       | ?A -> ?B -> _ => constr_eq_strict A B
+       end.
+  lazymatch type of prod with
+  | ?A -> ?B -> _ => constr_eq A B
+  end.
+  lazymatch type of prod with
+  | ?A -> ?B -> ?C => constr_eq A C
+  end.
+
+Abort.