Assume totality: dedicated type rather than bool

The rational is that

1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument

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