aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-17 08:19:49 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-17 08:19:49 +0200
commit0651bbfa273b2adc027ddd2cfb59df2fc5ea1330 (patch)
tree0e909cb9e6bac4e6b46127f88d2ae7d1611ed562 /test-suite
parentcee11fc609cb7d7087adabba389a97991e636219 (diff)
parent45e1e0dcba3101b6a9e096f18c28da899615af7f (diff)
Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/7615.v19
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7615.v b/test-suite/bugs/closed/7615.v
new file mode 100644
index 000000000..cd8c4ad7d
--- /dev/null
+++ b/test-suite/bugs/closed/7615.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+Module Type S.
+Parameter Inline T@{i} : Type@{i+1}.
+End S.
+
+Module F (X : S).
+Definition X@{j i} : Type@{j} := X.T@{i}.
+End F.
+
+Module M.
+Definition T@{i} := Type@{i}.
+End M.
+
+Module N := F(M).
+
+Require Import Hurkens.
+
+Fail Definition eqU@{i j} : @eq Type@{j} N.X@{i Set} Type@{i} := eq_refl.