aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-11 23:07:14 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-06-18 14:16:33 +0200
commit89a85a6603b7112e685a052d728284d3e4c2881e (patch)
treef3a3c51bd32439eeab9c2138d45a115adffa7850 /test-suite
parent0daf6af5949dbc7304e9fc3adf063519d5a60c4b (diff)
Fix #7421: constr_eq ignores universe constraints.
The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/7421.v39
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.