Fix mod_subst wrt universe polymorphism

1 files changed, 2 insertions, 1 deletions

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))