From e8bad8abc7be351a34fdf9770409bbab14bcd6a9 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Fri, 24 Jul 2015 08:46:09 +0200
Subject: Propagate `Guarded` flag from syntax to kernel.

The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
---
 library/global.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/global.ml')

diff --git a/library/global.ml b/library/global.ml
index 49fa2ef28..27f7f5266 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,8 +77,8 @@ let globalize_with_summary fs f =
 
 let i2l = Label.of_id
 
-let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a)
+let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set c = globalize0 (Safe_typing.push_context_set c)
 let push_context c = globalize0 (Safe_typing.push_context c)
-- 
cgit v1.2.3


From d4f3a1a807d474050a4e91e16ff7813f1db7f537 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Tue, 7 Jun 2016 09:52:43 +0200
Subject: 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
---
 intf/vernacexpr.mli         |  4 +--
 kernel/declarations.mli     | 13 ++++++++-
 kernel/declareops.ml        |  2 +-
 kernel/fast_typeops.ml      | 68 ++++++++++++++++++++++-----------------------
 kernel/fast_typeops.mli     |  7 +++--
 kernel/inductive.ml         |  8 +++---
 kernel/inductive.mli        |  4 +--
 kernel/safe_typing.ml       | 14 +++++-----
 kernel/safe_typing.mli      |  6 ++--
 kernel/term_typing.ml       | 34 +++++++++++------------
 kernel/term_typing.mli      | 10 +++----
 kernel/typeops.ml           |  4 +--
 library/assumptions.ml      |  2 +-
 library/declare.ml          | 18 ++++++------
 library/declare.mli         |  4 +--
 library/global.ml           |  4 +--
 library/global.mli          |  4 +--
 parsing/g_vernac.ml4        |  8 +++---
 plugins/funind/g_indfun.ml4 |  2 +-
 plugins/funind/indfun.ml    |  2 +-
 pretyping/inductiveops.ml   |  4 +--
 pretyping/pretyping.ml      |  6 ++--
 pretyping/typing.ml         |  4 +--
 printing/ppvernac.ml        |  8 +++---
 toplevel/command.ml         | 46 +++++++++++++++++-------------
 toplevel/command.mli        | 12 ++++----
 toplevel/vernacentries.ml   | 12 ++++----
 27 files changed, 164 insertions(+), 146 deletions(-)

(limited to 'library/global.ml')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ba9ac16b6..2f2f97376 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -307,10 +307,10 @@ type vernac_expr =
       bool (*[false] => assume positive*) *
       private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
-      bool * (* [false] => assume guarded *)
+      Declarations.typing_flags *
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
-      bool * (* [false] => assume guarded *)
+      Declarations.typing_flags *
       locality option * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 591a7d404..0c085df39 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -64,6 +64,15 @@ type constant_def =
 
 type constant_universes = Univ.universe_context
 
+(** The [typing_flags] are instructions to the type-checker which
+    modify its behaviour. The typing flags used in the type-checking
+    of a constant are tracked in their {!constant_body} so that they
+    can be displayed to the user. *)
+type typing_flags = {
+  check_guarded : bool; (** If [false] then fixed points and co-fixed
+                            points are assumed to be total. *)
+}
+
 (* some contraints are in constant_constraints, some other may be in
  * the OpaueDef *)
 type constant_body = {
@@ -75,7 +84,9 @@ type constant_body = {
     const_universes : constant_universes;
     const_proj : projection_body option;
     const_inline_code : bool;
-    const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *)
+    const_typing_flags : typing_flags; (** The typing options which
+                                           were used for
+                                           type-checking. *)
 }
 
 type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 068bc498a..98d287737 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -133,7 +133,7 @@ let subst_const_body sub cb =
         const_polymorphic = cb.const_polymorphic;
         const_universes = cb.const_universes;
         const_inline_code = cb.const_inline_code;
-        const_checked_guarded = cb.const_checked_guarded }
+        const_typing_flags = cb.const_typing_flags }
 
 (** {7 Hash-consing of constants } *)
 
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 8c14f5e04..32583f531 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -326,7 +326,7 @@ let type_fixpoint env lna lar vdef vdeft =
     (* ATTENTION : faudra faire le typage du contexte des Const,
     Ind et Constructsi un jour cela devient des constructions
     arbitraires et non plus des variables *)
-let rec execute ~chkguard env cstr =
+let rec execute ~flags env cstr =
   match kind_of_term cstr with
     (* Atomic terms *)
     | Sort (Prop c) ->
@@ -345,12 +345,12 @@ let rec execute ~chkguard env cstr =
       judge_of_constant env c
 	
     | Proj (p, c) ->
-        let ct = execute ~chkguard env c in
+        let ct = execute ~flags env c in
           judge_of_projection env p c ct
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-        let argst = execute_array ~chkguard env args in
+        let argst = execute_array ~flags env args in
 	let ft =
 	  match kind_of_term f with
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
@@ -363,7 +363,7 @@ let rec execute ~chkguard env cstr =
 	      judge_of_constant_knowing_parameters env cst args
 	  | _ ->
 	    (* Full or no sort-polymorphism *)
-	    execute ~chkguard env f
+            execute ~flags env f
 	in
 
 	  judge_of_apply env f ft args argst
@@ -371,25 +371,25 @@ let rec execute ~chkguard env cstr =
     | Lambda (name,c1,c2) ->
       let _ = execute_is_type env c1 in
       let env1 = push_rel (name,None,c1) env in
-      let c2t = execute ~chkguard env1 c2 in
+      let c2t = execute ~flags env1 c2 in
         judge_of_abstraction env name c1 c2t
 
     | Prod (name,c1,c2) ->
-      let vars = execute_is_type ~chkguard env c1 in
+      let vars = execute_is_type ~flags env c1 in
       let env1 = push_rel (name,None,c1) env in
-      let vars' = execute_is_type ~chkguard env1 c2 in
+      let vars' = execute_is_type ~flags env1 c2 in
 	judge_of_product env name vars vars'
 
     | LetIn (name,c1,c2,c3) ->
-      let c1t = execute ~chkguard env c1 in
+      let c1t = execute ~flags env c1 in
       let _c2s = execute_is_type env c2 in
       let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in
       let env1 = push_rel (name,Some c1,c2) env in
-      let c3t = execute ~chkguard env1 c3 in
+      let c3t = execute ~flags env1 c3 in
 	subst1 c1 c3t
 
     | Cast (c,k,t) ->
-      let ct = execute ~chkguard env c in
+      let ct = execute ~flags env c in
       let _ts = execute_type env t in
       let _ = judge_of_cast env c ct k t in
 	t
@@ -402,20 +402,20 @@ let rec execute ~chkguard env cstr =
       judge_of_constructor env c
 
     | Case (ci,p,c,lf) ->
-        let ct = execute ~chkguard env c in
-        let pt = execute ~chkguard env p in
-        let lft = execute_array ~chkguard env lf in
+        let ct = execute ~flags env c in
+        let pt = execute ~flags env p in
+        let lft = execute_array ~flags env lf in
           judge_of_case env ci p pt c ct lf lft
 
     | Fix ((vn,i as vni),recdef) ->
-      let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
+      let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
       let fix = (vni,recdef') in
-        check_fix env ~chk:chkguard fix; fix_ty
+        check_fix env ~flags fix; fix_ty
 	  
     | CoFix (i,recdef) ->
-      let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
+      let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
       let cofix = (i,recdef') in
-        check_cofix env ~chk:chkguard cofix; fix_ty
+        check_cofix env ~flags cofix; fix_ty
 	  
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
@@ -424,41 +424,41 @@ let rec execute ~chkguard env cstr =
     | Evar _ ->
 	anomaly (Pp.str "the kernel does not support existential variables")
 
-and execute_is_type ~chkguard env constr =
-  let t = execute ~chkguard env constr in
+and execute_is_type ~flags env constr =
+  let t = execute ~flags env constr in
     check_type env constr t
 
-and execute_type ~chkguard env constr =
-  let t = execute ~chkguard env constr in
+and execute_type ~flags env constr =
+  let t = execute ~flags env constr in
     type_judgment env constr t
 
-and execute_recdef ~chkguard env (names,lar,vdef) i =
-  let lart = execute_array ~chkguard env lar in
+and execute_recdef ~flags env (names,lar,vdef) i =
+  let lart = execute_array ~flags env lar in
   let lara = Array.map2 (assumption_of_judgment env) lar lart in
   let env1 = push_rec_types (names,lara,vdef) env in
-  let vdeft = execute_array ~chkguard env1 vdef in
+  let vdeft = execute_array ~flags env1 vdef in
   let () = type_fixpoint env1 names lara vdef vdeft in
     (lara.(i),(names,lara,vdef))
 
-and execute_array ~chkguard env = Array.map (execute ~chkguard env)
+and execute_array ~flags env = Array.map (execute ~flags env)
 
 (* Derived functions *)
-let infer ~chkguard env constr =
-  let t = execute ~chkguard env constr in
+let infer ~flags env constr =
+  let t = execute ~flags env constr in
     make_judge constr t
 
 let infer = 
   if Flags.profile then
     let infer_key = Profile.declare_profile "Fast_infer" in
-      Profile.profile3 infer_key (fun a b c -> infer ~chkguard:a b c)
-  else (fun a b c -> infer ~chkguard:a b c)
+      Profile.profile3 infer_key (fun a b c -> infer ~flags:a b c)
+  else (fun a b c -> infer ~flags:a b c)
 
 (* Restores the labels of [infer] lost to profiling. *)
-let infer ~chkguard env t = infer chkguard env t
+let infer ~flags env t = infer flags env t
 
-let infer_type ~chkguard env constr =
-  execute_type ~chkguard env constr
+let infer_type ~flags env constr =
+  execute_type ~flags env constr
 
-let infer_v ~chkguard env cv =
-  let jv = execute_array ~chkguard env cv in
+let infer_v ~flags env cv =
+  let jv = execute_array ~flags env cv in
     make_judgev cv jv
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 98dbefad1..1c0146bae 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -8,6 +8,7 @@
 
 open Term
 open Environ
+open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
     
@@ -18,6 +19,6 @@ open Environ
  *)
 
 
-val infer      : chkguard:bool -> env -> constr       -> unsafe_judgment
-val infer_v    : chkguard:bool -> env -> constr array -> unsafe_judgment array
-val infer_type : chkguard:bool -> env -> types        -> unsafe_type_judgment
+val infer      : flags:typing_flags -> env -> constr       -> unsafe_judgment
+val infer_v    : flags:typing_flags -> env -> constr array -> unsafe_judgment array
+val infer_type : flags:typing_flags -> env -> types        -> unsafe_type_judgment
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 532287c30..fdca5ce26 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1065,8 +1065,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   (Array.map fst rv, Array.map snd rv)
 
 
-let check_fix env ~chk ((nvect,_),(names,_,bodies as recdef) as fix) =
-  if chk then
+let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) =
+  if flags.check_guarded then
     let (minds, rdef) = inductive_of_mutfix env fix in
     let get_tree (kn,i) =
       let mib = Environ.lookup_mind kn env in
@@ -1193,8 +1193,8 @@ let check_one_cofix env nbfix def deftype =
 (* The  function which checks that the whole block of definitions
    satisfies the guarded condition *)
 
-let check_cofix env ~chk (bodynum,(names,types,bodies as recdef)) =
-  if chk then
+let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) =
+  if flags.check_guarded then
     let nbfix = Array.length bodies in
     for i = 0 to nbfix-1 do
       let fixenv = push_rec_types recdef env in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 36f32b30c..54036d86a 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -98,8 +98,8 @@ val check_case_info : env -> pinductive -> case_info -> unit
 
 (** When [chk] is false, the guard condition is not actually
     checked. *)
-val check_fix : env -> chk:bool -> fixpoint -> unit
-val check_cofix : env -> chk:bool -> cofixpoint -> unit
+val check_fix : env -> flags:typing_flags -> fixpoint -> unit
+val check_cofix : env -> flags:typing_flags -> cofixpoint -> unit
 
 (** {6 Support for sort-polymorphic inductive types } *)
 
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
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 80b9bb495..c5e43e42a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -57,16 +57,16 @@ val is_joined_environment : safe_environment -> bool
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0
 val push_named_def :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   Id.t * Entries.definition_entry -> safe_transformer0
 
 (** Insertion of global axioms or definitions *)
 
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry * bool (* chkguard *)
+  | ConstantEntry of Entries.constant_entry * Declarations.typing_flags
   | GlobalRecipe of Cooking.recipe
 
 val add_constant :
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8a105ac97..64597469a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -23,18 +23,18 @@ open Entries
 open Typeops
 open Fast_typeops
 
-let constrain_type ~chkguard env j poly subst = function
+let constrain_type ~flags env j poly subst = function
   | `None -> 
     if not poly then (* Old-style polymorphism *)
       make_polymorphic_if_constant_for_ind env j
     else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
   | `Some t ->
-      let tj = infer_type ~chkguard env t in
+      let tj = infer_type ~flags env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
   | `SomeWJ (t, tj) ->
-      let tj = infer_type ~chkguard env t in
+      let tj = infer_type ~flags env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
@@ -101,11 +101,11 @@ let hcons_j j =
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
 
-let infer_declaration ~chkguard env kn dcl =
+let infer_declaration ~flags env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context uctx env in
-      let j = infer ~chkguard env t in
+      let j = infer ~flags env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
       let c = Typeops.assumption_of_judgment env j in
@@ -122,7 +122,7 @@ let infer_declaration ~chkguard env kn dcl =
         Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
           let body = handle_side_effects env body side_eff in
 	  let env' = push_context_set ctx env in
-          let j = infer ~chkguard env' body in
+          let j = infer ~flags env' body in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
           let _typ = constrain_type env' j c.const_entry_polymorphic subst
@@ -143,8 +143,8 @@ let infer_declaration ~chkguard env kn dcl =
       let body = handle_side_effects env body side_eff in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
-      let j = infer ~chkguard env body in
-      let typ = constrain_type ~chkguard env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+      let j = infer ~flags env body in
+      let typ = constrain_type ~flags env j c.const_entry_polymorphic usubst (map_option_typ typ) in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
 	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
@@ -186,7 +186,7 @@ let record_aux env s1 s2 =
 let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
 let set_suggest_proof_using f = suggest_proof_using := f
 
-let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) =
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -262,25 +262,25 @@ let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_
     const_polymorphic = poly;
     const_universes = univs;
     const_inline_code = inline_code;
-    const_checked_guarded = chkguard }
+    const_typing_flags = flags }
 
 
 (*s Global and local constant declaration. *)
 
-let translate_constant ~chkguard env kn ce =
-  build_constant_declaration ~chkguard kn env (infer_declaration ~chkguard env (Some kn) ce)
+let translate_constant ~flags env kn ce =
+  build_constant_declaration ~flags kn env (infer_declaration ~flags env (Some kn) ce)
 
-let translate_local_assum ~chkguard env t =
-  let j = infer ~chkguard env t in
+let translate_local_assum ~flags env t =
+  let j = infer ~flags env t in
   let t = Typeops.assumption_of_judgment env j in
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration ~chkguard:true kn env (Cooking.cook_constant env r)
+  build_constant_declaration ~flags:{check_guarded=true} kn env (Cooking.cook_constant env r)
 
-let translate_local_def ~chkguard env id centry =
+let translate_local_def ~flags env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
-    infer_declaration ~chkguard env None (DefinitionEntry centry) in
+    infer_declaration ~flags env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
   def, typ, univs
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index ba4d96a5f..f167603a7 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,10 +12,10 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : chkguard:bool -> env -> Id.t -> definition_entry ->
+val translate_local_def : flags:typing_flags -> env -> Id.t -> definition_entry ->
   constant_def * types * constant_universes
 
-val translate_local_assum : chkguard:bool -> env -> types -> types
+val translate_local_assum : flags:typing_flags -> env -> types -> types
 
 val mk_pure_proof : constr -> proof_output
 
@@ -28,7 +28,7 @@ val handle_entry_side_effects : env -> definition_entry -> definition_entry
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val translate_constant : chkguard:bool -> env -> constant -> constant_entry -> constant_body
+val translate_constant : flags:typing_flags -> env -> constant -> constant_entry -> constant_body
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,11 +37,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : chkguard:bool -> env -> constant option -> 
+val infer_declaration : flags:typing_flags -> env -> constant option ->
   constant_entry -> Cooking.result
 
 val build_constant_declaration :
-  chkguard:bool -> constant -> env -> Cooking.result -> constant_body
+  flags:typing_flags -> constant -> env -> Cooking.result -> constant_body
 
 val set_suggest_proof_using :
   (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 9e9f18aaa..1c3117725 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -494,13 +494,13 @@ let rec execute env cstr =
     | Fix ((vn,i as vni),recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let fix = (vni,recdef') in
-        check_fix ~chk:true env fix;
+        check_fix ~flags:{check_guarded=true} env fix;
 	make_judge (mkFix fix) fix_ty
 	  
     | CoFix (i,recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let cofix = (i,recdef') in
-        check_cofix ~chk:true env cofix;
+        check_cofix ~flags:{check_guarded=true} env cofix;
 	(make_judge (mkCoFix cofix) fix_ty)
 	  
     (* Partial proofs: unsupported by the kernel *)
diff --git a/library/assumptions.ml b/library/assumptions.ml
index 463527820..f374f6dbe 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -227,7 +227,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
   | ConstRef kn ->
       let cb = lookup_constant kn in
       let accu =
-        if cb.const_checked_guarded then accu
+        if cb.const_typing_flags.check_guarded then accu
         else ContextObjectMap.add (Axiom (Guarded kn)) Constr.mkProp accu
       in
     if not (Declareops.constant_has_body cb) then
diff --git a/library/declare.ml b/library/declare.ml
index 4be13109a..c49284bbc 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -50,11 +50,11 @@ let cache_variable ((sp,_),o) =
 
   let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ~chkguard:true ((id,ty),ctx) in
+      let () = Global.push_named_assum ~flags:{check_guarded=true} ((id,ty),ctx) in
       let impl = if impl then Implicit else Explicit in
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
-      let () = Global.push_named_def ~chkguard:true (id,de) in
+      let () = Global.push_named_def ~flags:{check_guarded=true} (id,de) in
         Explicit, de.const_entry_opaque, de.const_entry_polymorphic, 
 	(Univ.ContextSet.of_context de.const_entry_universes) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
@@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) =
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = 
-  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), true)
+  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), {check_guarded=true})
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
@@ -232,7 +232,7 @@ let declare_sideff env fix_exn se =
         const_entry_feedback = None;
 	const_entry_polymorphic = cb.const_polymorphic;
 	const_entry_universes = univs;
-      }, true);
+      }, {check_guarded=true});
     cst_hyps = [] ;
     cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
     cst_locl = true;
@@ -253,7 +253,7 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(flags={check_guarded=true}) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let cd = (* We deal with side effects *)
     match cd with
     | Entries.DefinitionEntry de ->
@@ -275,7 +275,7 @@ let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false)
     | _ -> cd
   in
   let cst = {
-    cst_decl = ConstantEntry (cd,chkguard);
+    cst_decl = ConstantEntry (cd,flags);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
@@ -283,13 +283,13 @@ let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false)
   let kn = declare_constant_common id cst in
   kn
 
-let declare_definition ?chkguard ?(internal=UserVerbose) 
+let declare_definition ?flags ?(internal=UserVerbose)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
   let cb = 
     definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
-    declare_constant ?chkguard ~internal ~local id
+    declare_constant ?flags ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of inductive blocks *)
@@ -387,7 +387,7 @@ let declare_projections mind =
       Array.iteri (fun i kn -> 
 	let id = Label.to_id (Constant.label kn) in
 	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
-	let kn' = declare_constant ~chkguard:true id (ProjectionEntry entry,
+        let kn' = declare_constant ~flags:{check_guarded=true} id (ProjectionEntry entry,
 				       IsDefinition StructureComponent) 
 	in
 	  assert(eq_constant kn kn')) kns; true
diff --git a/library/declare.mli b/library/declare.mli
index 94cebe3bd..cda8855d2 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,11 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
   constr -> definition_entry
 
 val declare_constant :
-  ?chkguard:bool -> (** default [true] (check guardedness) *)
+  ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *)
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
-  ?chkguard:bool -> (** default [true] (check guardedness) *)
+  ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *)
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
diff --git a/library/global.ml b/library/global.ml
index 27f7f5266..ab326e37d 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,8 +77,8 @@ let globalize_with_summary fs f =
 
 let i2l = Label.of_id
 
-let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a)
-let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d)
+let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a)
+let push_named_def ~flags d = globalize0 (Safe_typing.push_named_def ~flags d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set c = globalize0 (Safe_typing.push_context_set c)
 let push_context c = globalize0 (Safe_typing.push_context c)
diff --git a/library/global.mli b/library/global.mli
index 388fee527..f7306fe57 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,9 +32,9 @@ val set_type_in_type : unit -> unit
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : 
-  chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit
+  flags:Declarations.typing_flags -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit
 val push_named_def   :
-  chkguard:bool -> (Id.t * Entries.definition_entry) -> unit
+  flags:Declarations.typing_flags -> (Id.t * Entries.definition_entry) -> unit
 
 val add_constant :
   DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ced2da7a5..3ad5e77fc 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -219,13 +219,13 @@ GEXTEND Gram
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
           VernacInductive (check_positivity a,priv,f,indl)
       | "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (check_guardedness a,None, recs)
+          VernacFixpoint ({Declarations.check_guarded=check_guardedness a},None, recs)
       | IDENT "Let"; "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (check_guardedness a,Some Discharge, recs)
+          VernacFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, recs)
       | "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (check_guardedness a,None, corecs)
+          VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},None, corecs)
       | IDENT "Let"; "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (check_guardedness a,Some Discharge, corecs)
+          VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, corecs)
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	      l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 53ec304cc..91fcb3f8b 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function
            | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
          match
            Vernac_classifier.classify_vernac
-             (Vernacexpr.VernacFixpoint(true,None, List.map snd recsl))
+             (Vernacexpr.VernacFixpoint({Declarations.check_guarded=true},None, List.map snd recsl))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
              Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 5c849ba41..0ea90ecd1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -399,7 +399,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       Command.do_fixpoint ~chkguard:true Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       Command.do_fixpoint ~flags:{Declarations.check_guarded=true} Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
 	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index efea4bec8..930b0413e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -593,9 +593,9 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
 let control_only_guard env c =
   let check_fix_cofix e c = match kind_of_term c with
     | CoFix (_,(_,_,_) as cofix) ->
-	Inductive.check_cofix ~chk:true e cofix
+      Inductive.check_cofix ~flags:{check_guarded=true} e cofix
     | Fix (_,(_,_,_) as fix) ->
-	Inductive.check_fix ~chk:true e fix
+      Inductive.check_fix ~flags:{check_guarded=true} e fix
     | _ -> ()
   in
   let rec iter env c =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d9f490ba5..8fbcc8e5e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -75,7 +75,7 @@ let search_guard loc env possible_indexes fixdefs =
   if List.for_all is_singleton possible_indexes then
     let indexes = Array.of_list (List.map List.hd possible_indexes) in
     let fix = ((indexes, 0),fixdefs) in
-    (try check_fix env ~chk:true fix
+    (try check_fix env ~flags:{Declarations.check_guarded=true} fix
      with reraise ->
        let (e, info) = Errors.push reraise in
        let info = Loc.add_loc info loc in
@@ -88,7 +88,7 @@ let search_guard loc env possible_indexes fixdefs =
 	 (fun l ->
 	    let indexes = Array.of_list l in
 	    let fix = ((indexes, 0),fixdefs) in
-	    try check_fix env ~chk:true fix; raise (Found indexes)
+            try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes)
 	    with TypeError _ -> ())
 	 (List.combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
@@ -537,7 +537,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	    make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	| GCoFix i ->
 	  let cofix = (i,(names,ftys,fdefs)) in
-	    (try check_cofix env ~chk:true cofix
+            (try check_cofix env ~flags:{Declarations.check_guarded=true} cofix
              with reraise ->
                let (e, info) = Errors.push reraise in
                let info = Loc.add_loc info loc in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 0bb2979c2..fa6fd9677 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -184,13 +184,13 @@ let rec execute env evdref cstr =
     | Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
 	let fix = (vni,recdef') in
-        check_fix env ~chk:true fix;
+        check_fix env ~flags:{Declarations.check_guarded=true} fix;
 	make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
         let cofix = (i,recdef') in
-        check_cofix env ~chk:true cofix;
+        check_cofix env ~flags:{Declarations.check_guarded=true} cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop c) ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 93cd35472..8a8521ccc 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -806,7 +806,7 @@ module Make
               (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
           )
 
-        | VernacFixpoint (chkguard,local, recs) ->
+        | VernacFixpoint (flags,local, recs) ->
           let local = match local with
             | Some Discharge -> "Let "
             | Some Local -> "Local "
@@ -821,11 +821,11 @@ module Make
                 prlist (pr_decl_notation pr_constr) ntn
           in
           return (
-            hov 0 (pr_assume ~guarded:chkguard ()++str local ++ keyword "Fixpoint" ++ spc () ++
+            hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++str local ++ keyword "Fixpoint" ++ spc () ++
                      prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs)
           )
 
-        | VernacCoFixpoint (chkguard,local, corecs) ->
+        | VernacCoFixpoint (flags,local, corecs) ->
           let local = match local with
             | Some Discharge -> keyword "Let" ++ spc ()
             | Some Local -> keyword "Local" ++ spc ()
@@ -838,7 +838,7 @@ module Make
               prlist (pr_decl_notation pr_constr) ntn
           in
           return (
-            hov 0 (pr_assume ~guarded:chkguard ()++local ++ keyword "CoFixpoint" ++ spc() ++
+            hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++local ++ keyword "CoFixpoint" ++ spc() ++
                      prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
           )
         | VernacScheme l ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c6d67b13a..b6dd2718f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -139,9 +139,9 @@ let get_locality id = function
 | Local -> true
 | Global -> false
 
-let declare_global_definition ~chkguard ident ce local k imps =
+let declare_global_definition ~flags ident ce local k imps =
   let local = get_locality ident local in
-  let kn = declare_constant ~chkguard ident ~local (DefinitionEntry ce, IsDefinition k) in
+  let kn = declare_constant ~flags ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = definition_message ident in
@@ -151,7 +151,7 @@ let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
-let declare_definition ~chkguard ident (local, p, k) ce imps hook =
+let declare_definition ~flags ident (local, p, k) ce imps hook =
   let () = !declare_definition_hook ce in
   let r = match local with
   | Discharge when Lib.sections_are_opened () ->
@@ -167,10 +167,11 @@ let declare_definition ~chkguard ident (local, p, k) ce imps hook =
     in
     gr
   | Discharge | Local | Global ->
-    declare_global_definition ~chkguard ident ce local k imps in
+    declare_global_definition ~flags ident ce local k imps in
   Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
 
-let _ = Obligations.declare_definition_ref := declare_definition ~chkguard:true
+let _ = Obligations.declare_definition_ref :=
+    declare_definition ~flags:{Declarations.check_guarded=true}
 
 let do_definition ident k bl red_option c ctypopt hook =
   let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
@@ -191,7 +192,7 @@ let do_definition ident k bl red_option c ctypopt hook =
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ~chkguard:true ident k ce imps
+      ignore(declare_definition ~flags:{Declarations.check_guarded=true} ident k ce imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -752,11 +753,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix ~chkguard ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
+let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition ~chkguard f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
+  declare_definition ~flags f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
 
-let _ = Obligations.declare_fix_ref := (declare_fix ~chkguard:true)
+let _ = Obligations.declare_fix_ref :=
+    (declare_fix ~flags:{Declarations.check_guarded=true})
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1044,7 +1046,7 @@ let interp_cofixpoint l ntns =
   check_recursive false  env evd fix;
   fix,Evd.evar_universe_context evd,info
     
-let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
+let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1072,7 +1074,7 @@ let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fixim
     let ctx = Universes.restrict_universe_context ctx vars in
     let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let ctx = Univ.ContextSet.to_context ctx in
-    ignore (List.map4 (declare_fix ~chkguard (local, poly, Fixpoint) ctx)
+    ignore (List.map4 (declare_fix ~flags (local, poly, Fixpoint) ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1080,7 +1082,7 @@ let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fixim
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
+let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1103,7 +1105,7 @@ let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fix
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
     let ctx = Univ.ContextSet.to_context ctx in
-    ignore (List.map4 (declare_fix ~chkguard (local, poly, CoFixpoint) ctx) 
+    ignore (List.map4 (declare_fix ~flags (local, poly, CoFixpoint) ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1168,7 +1170,11 @@ let do_program_recursive local p fixkind fixl ntns =
       in
       let indexes = 
 	Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
-	List.iteri (fun i _ -> Inductive.check_fix env ~chk:true ((indexes,i),fixdecls)) fixl
+      List.iteri (fun i _ ->
+          Inductive.check_fix env
+                              ~flags:{Declarations.check_guarded=true}
+                              ((indexes,i),fixdecls))
+        fixl
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
@@ -1202,21 +1208,21 @@ let do_program_fixpoint local poly l =
 	errorlabstrm "do_program_fixpoint"
 	  (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_fixpoint ~chkguard local poly l =
+let do_fixpoint ~flags local poly l =
   if Flags.is_program_mode () then do_program_fixpoint local poly l
   else
     let fixl, ntns = extract_fixpoint_components true l in
     let fix = interp_fixpoint fixl ntns in
     let possible_indexes =
       List.map compute_possible_guardness_evidences (pi3 fix) in
-    declare_fixpoint ~chkguard local poly fix possible_indexes ntns;
-    if not chkguard then Pp.feedback Feedback.AddedAxiom else ()
+    declare_fixpoint ~flags local poly fix possible_indexes ntns;
+    if not flags.Declarations.check_guarded then Pp.feedback Feedback.AddedAxiom else ()
 
-let do_cofixpoint ~chkguard local poly l =
+let do_cofixpoint ~flags local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
     if Flags.is_program_mode () then
       do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns
     else
       let cofix = interp_cofixpoint fixl ntns in
-      declare_cofixpoint ~chkguard local poly cofix ntns;
-      if not chkguard then Pp.feedback Feedback.AddedAxiom else ()
+      declare_cofixpoint ~flags local poly cofix ntns;
+      if not flags.Declarations.check_guarded then Pp.feedback Feedback.AddedAxiom else ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 7578e26c1..73f8f9806 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -34,7 +34,7 @@ val interp_definition :
   local_binder list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
-val declare_definition : chkguard:bool ->
+val declare_definition : flags:Declarations.typing_flags ->
   Id.t -> definition_kind ->
   definition_entry -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
@@ -147,14 +147,14 @@ val interp_cofixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   locality -> polymorphic ->
   recursive_preentry * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
-  chkguard:bool -> locality -> polymorphic ->
+  flags:Declarations.typing_flags -> locality -> polymorphic ->
   recursive_preentry * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
@@ -162,11 +162,11 @@ val declare_cofixpoint :
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
-  chkguard:bool -> (* When [false], assume guarded. *)
+  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
-  chkguard:bool -> (* When [false], assume guarded. *)
+  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (** Utils *)
@@ -174,6 +174,6 @@ val do_cofixpoint :
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
 val declare_fix :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
   Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a0af1d573..40dfa1b9a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -578,17 +578,17 @@ let vernac_inductive chk poly lo finite indl =
     let indl = List.map unpack indl in
     do_mutual_inductive chk indl poly lo finite
 
-let vernac_fixpoint ~chkguard locality poly local l =
+let vernac_fixpoint ~flags locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_fixpoint ~chkguard local poly l
+  do_fixpoint ~flags local poly l
 
-let vernac_cofixpoint ~chkguard locality poly local l =
+let vernac_cofixpoint ~flags locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_cofixpoint ~chkguard local poly l
+  do_cofixpoint ~flags local poly l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1895,8 +1895,8 @@ let interp ?proof locality poly c =
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
   | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l
-  | VernacFixpoint (chkguard,local, l) -> vernac_fixpoint ~chkguard locality poly local l
-  | VernacCoFixpoint (chkguard,local, l) -> vernac_cofixpoint ~chkguard locality poly local l
+  | VernacFixpoint (flags,local, l) -> vernac_fixpoint ~flags locality poly local l
+  | VernacCoFixpoint (flags,local, l) -> vernac_cofixpoint ~flags locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe l
-- 
cgit v1.2.3