diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 036555309f..62753962c8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -231,11 +231,11 @@ let constant_entry_of_private_constant = function let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in - { Entries.from_env = Ephemeron.create env.revstruct; + { Entries.from_env = CEphemeron.create env.revstruct; Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } let private_con_of_scheme ~kind env cl = - { Entries.from_env = Ephemeron.create env.revstruct; + { Entries.from_env = CEphemeron.create env.revstruct; Entries.eff = Entries.SEscheme( List.map (fun (i,c) -> let cbo = Environ.lookup_constant c env.env in @@ -561,6 +561,7 @@ let add_mind dir l mie senv = let add_modtype l params_mte inl senv = let mp = MPdot(senv.modpath, l) in let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte in + let mtb = Declareops.hcons_module_body mtb in let senv' = add_field (l,SFBmodtype mtb) MT senv in mp, senv' @@ -581,6 +582,7 @@ let full_add_module_type mp mt senv = let add_module l me inl senv = let mp = MPdot(senv.modpath, l) in let mb = Mod_typing.translate_module senv.env mp inl me in + let mb = Declareops.hcons_module_body mb in let senv' = add_field (l,SFBmodule mb) M senv in let senv'' = if Modops.is_functor mb.mod_type then senv' |