diff options
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r-- | kernel/safe_typing.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ce05190b6..72d6ee518 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -373,8 +373,8 @@ let safe_push_named d env = Environ.push_named d env -let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in +let push_named_def ~flags (id,de) senv = + let c,typ,univs = Term_typing.translate_local_def ~flags senv.revstruct senv.env id de in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -388,9 +388,9 @@ let push_named_def (id,de) senv = let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in univs, {senv' with env=env''} -let push_named_assum ((id,t,poly),ctx) senv = +let push_named_assum ~flags ((id,t,poly),ctx) senv = let senv' = push_context_set poly ctx senv in - let t = Term_typing.translate_local_assum senv'.env t in + let t = Term_typing.translate_local_assum ~flags senv'.env t in let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in {senv' with env=env''} @@ -479,7 +479,7 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe type exported_private_constant = @@ -512,10 +512,10 @@ let add_constant dir l decl senv = let no_section = DirPath.is_empty dir in let seff_to_export, decl = match decl with - | ConstantEntry (true, ce) -> + | ConstantEntry (true, ce, flags) -> let exports, ce = - Term_typing.export_side_effects senv.revstruct senv.env ce in - exports, ConstantEntry (false, ce) + Term_typing.export_side_effects ~flags senv.revstruct senv.env ce in + exports, ConstantEntry (false, ce, flags) | _ -> [], decl in let senv = @@ -524,8 +524,8 @@ let add_constant dir l decl senv = let senv = let cb = match decl with - | ConstantEntry (export_seff,ce) -> - Term_typing.translate_constant senv.revstruct senv.env kn ce + | ConstantEntry (export_seff,ce,flags) -> + Term_typing.translate_constant ~flags senv.revstruct senv.env kn ce | GlobalRecipe r -> let cb = Term_typing.translate_recipe senv.env kn r in if no_section then Declareops.hcons_const_body cb else cb in |