diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-28 01:00:23 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-07 13:18:50 +0200 |
commit | e398b8b5dadb0cd75cd6cfb86525ccb039d75d49 (patch) | |
tree | b75f75b6bf98babcb7163194b2e716f2ca53eb7c /test-suite/bugs | |
parent | 28ca5295339afecfc4ecb70214f6f575c11e34a1 (diff) |
Fix #7615: Functor inlining drops universe substitution.
We store the universe context in the inlined terms and apply it to
the instance provided to the substitution function. Technically the
context is not needed, but we use it to assert that the length of the
instance corresponds, just in case.
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/7615.v | 19 |
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. |