diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 18d897817..2cea50d9e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env = Environ.push_named d env -let push_named_def ~chkguard (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in +let push_named_def ~flags (id,de) senv = + let c,typ,univs = Term_typing.translate_local_def ~flags senv.env id de in let senv' = push_context univs senv in let c, senv' = match c with | Def c -> Mod_subst.force_constr c, senv' @@ -346,9 +346,9 @@ let push_named_def ~chkguard (id,de) senv = let env'' = safe_push_named (id,Some c,typ) senv'.env in {senv' with env=env''} -let push_named_assum ~chkguard ((id,t),ctx) senv = +let push_named_assum ~flags ((id,t),ctx) senv = let senv' = push_context_set ctx senv in - let t = Term_typing.translate_local_assum ~chkguard senv'.env t in + let t = Term_typing.translate_local_assum ~flags senv'.env t in let env'' = safe_push_named (id,None,t) senv'.env in {senv' with env=env''} @@ -439,14 +439,14 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of Entries.constant_entry * bool (* check guard *) + | ConstantEntry of Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe let add_constant dir l decl senv = let kn = make_con senv.modpath dir l in let cb = match decl with - | ConstantEntry (ce,chkguard) -> - Term_typing.translate_constant ~chkguard senv.env kn ce + | ConstantEntry (ce,flags) -> + Term_typing.translate_constant ~flags senv.env kn ce | GlobalRecipe r -> let cb = Term_typing.translate_recipe senv.env kn r in if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb |