diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 3 |
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)) |