From e398b8b5dadb0cd75cd6cfb86525ccb039d75d49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 28 May 2018 01:00:23 +0200 Subject: 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. --- test-suite/bugs/closed/7615.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 test-suite/bugs/closed/7615.v (limited to 'test-suite/bugs') 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. -- cgit v1.2.3