diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 0182b3907..1ca0fec4a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -132,15 +132,15 @@ let hcons_constant_body cb = let add_constant dir l decl senv = check_label l senv.labset; - let cb = match decl with - ConstantEntry ce -> translate_constant senv.env ce + let kn = make_kn senv.modinfo.modpath dir l in + let cb = + match decl with + | ConstantEntry ce -> translate_constant senv.env kn ce | GlobalRecipe r -> - let cb = translate_recipe senv.env r in - if dir = empty_dirpath then hcons_constant_body cb else cb + let cb = translate_recipe senv.env kn r in + if dir = empty_dirpath then hcons_constant_body cb else cb in -(* let cb = if dir = empty_dirpath then hcons_constant_body cb else cb in*) let env' = Environ.add_constraints cb.const_constraints senv.env in - let kn = make_kn senv.modinfo.modpath dir l in let env'' = Environ.add_constant kn cb env' in kn, { old = senv.old; env = env''; @@ -417,7 +417,6 @@ let check_engagement env c = let set_engagement c senv = {senv with env = Environ.set_engagement c senv.env} - (* Libraries = Compiled modules *) type compiled_library = |