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.
---
 kernel/modops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 2038171183..22f523a9ae 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	    | Undef _ | OpaqueDef _ -> l
 	    | Def body ->
 	      let constr = Mod_subst.force_constr body in
-	      add_inline_delta_resolver kn (lev, Some constr) l
+              let ctx = Declareops.constant_polymorphic_context constant in
+              add_inline_delta_resolver kn (lev, Some (ctx, constr)) l
 	with Not_found ->
 	  error_no_such_label_sub (Constant.label con)
 	    (ModPath.to_string (Constant.modpath con))
-- 
cgit v1.2.3