From 470943bdf917caf352b5347c8d33fc39699805b0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Nov 2018 12:55:46 +0100
Subject: Fix mod_subst wrt universe polymorphism

---
 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 f43dbd88f9..97ac3cdebb 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	    | Def body ->
 	      let constr = Mod_subst.force_constr body in
               let ctx = Declareops.constant_polymorphic_context constant in
-              add_inline_delta_resolver kn (lev, Some (ctx, constr)) l
+              let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in
+              add_inline_delta_resolver kn (lev, Some constr) l
 	with Not_found ->
 	  error_no_such_label_sub (Constant.label con)
 	    (ModPath.to_string (Constant.modpath con))
-- 
cgit v1.2.3