From 89a85a6603b7112e685a052d728284d3e4c2881e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 11 May 2018 23:07:14 +0200
Subject: Fix #7421: constr_eq ignores universe constraints.

The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
---
 test-suite/bugs/closed/7421.v | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 test-suite/bugs/closed/7421.v

(limited to 'test-suite/bugs')

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.
-- 
cgit v1.2.3