diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index e04eb354e..392e667b8 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver = in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) } + const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) } let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then mb |