Factorizing the uses of Declareops.safe_flags.

This allows a smooth addition of various unsafe flags without wreaking
havoc in the ML codebase.

12 files changed, 26 insertions, 26 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8d74dc390..f0c116d27 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -471,7 +471,7 @@ let translate_local_assum ~flags env t =
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration ~flags:{check_guarded=true} kn env (Cooking.cook_constant env r)
+  build_constant_declaration ~flags:Declareops.safe_flags kn env (Cooking.cook_constant env r)
 
 let translate_local_def ~flags mb env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a94a049df..9b9792ce8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -500,13 +500,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 ~flags:{check_guarded=true} env fix;
+        check_fix ~flags:Declareops.safe_flags 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 ~flags:{check_guarded=true} env cofix;
+        check_cofix ~flags:Declareops.safe_flags env cofix;
 	(make_judge (mkCoFix cofix) fix_ty)
 	  
     (* Partial proofs: unsupported by the kernel *)
diff --git a/library/declare.ml b/library/declare.ml
index 9ec299bed..335263f8f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -58,11 +58,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 ~flags:{check_guarded=true} ((id,ty,poly),ctx) in
+      let () = Global.push_named_assum ~flags:Declareops.safe_flags ((id,ty,poly),ctx) in
       let impl = if impl then Implicit else Explicit in
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
-      let univs = Global.push_named_def ~flags:{check_guarded=true} (id,de) in
+      let univs = Global.push_named_def ~flags:Declareops.safe_flags (id,de) in
       Explicit, de.const_entry_opaque,
       de.const_entry_polymorphic, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
@@ -180,7 +180,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
-    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), {check_guarded=true})
+    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), Declareops.safe_flags)
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
@@ -246,7 +246,7 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let declare_constant ?(flags={check_guarded=true}) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let export = (* We deal with side effects *)
     match cd with
     | DefinitionEntry de when
@@ -374,7 +374,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 ~flags:{check_guarded=true} id (ProjectionEntry entry,
+	let kn' = declare_constant ~flags:Declareops.safe_flags id (ProjectionEntry entry,
 				       IsDefinition StructureComponent)
 	in
 	  assert(eq_constant kn kn')) kns; true,true
diff --git a/library/declare.mli b/library/declare.mli
index 3ba63b5a6..41221d5c9 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -54,11 +54,11 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 val declare_constant :
-  ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *)
+  ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *)
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
-  ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *)
+  ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *)
   ?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/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d8340dddb..8b3d3dc20 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -400,7 +400,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       Command.do_fixpoint ~flags:{Declarations.check_guarded=true} Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       Command.do_fixpoint ~flags:Declareops.safe_flags 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 0b488308a..1d7720454 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -592,9 +592,9 @@ let type_of_projection_knowing_arg env sigma p c ty =
 let control_only_guard env c =
   let check_fix_cofix e c = match kind_of_term c with
     | CoFix (_,(_,_,_) as cofix) ->
-      Inductive.check_cofix ~flags:{check_guarded=true} e cofix
+      Inductive.check_cofix ~flags:Declareops.safe_flags e cofix
     | Fix (_,(_,_,_) as fix) ->
-      Inductive.check_fix ~flags:{check_guarded=true} e fix
+      Inductive.check_fix ~flags:Declareops.safe_flags e fix
     | _ -> ()
   in
   let rec iter env c =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c894d96a7..65f5b3fd0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -101,7 +101,7 @@ let search_guard ~tflags loc env possible_indexes fixdefs =
                will be chosen). A more robust solution may be to raise an
                error when totality is assumed but the strutural argument is
                not specified. *)
-            try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes)
+            try check_fix env ~flags:Declareops.safe_flags fix; raise (Found indexes)
 	    with TypeError _ -> ())
 	 (List.combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
@@ -617,13 +617,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	  let fixdecls = (names,ftys,fdefs) in
           let indexes =
             search_guard
-              ~tflags:{Declarations.check_guarded=true}
+              ~tflags:Declareops.safe_flags
               loc env possible_indexes fixdecls
           in
 	    make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	| GCoFix i ->
 	  let cofix = (i,(names,ftys,fdefs)) in
-            (try check_cofix env ~flags:{Declarations.check_guarded=true} cofix
+            (try check_cofix env ~flags:Declareops.safe_flags 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 598dd16d0..f03e6c6e9 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -189,13 +189,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 ~flags:{Declarations.check_guarded=true} fix;
+        check_fix env ~flags:Declareops.safe_flags 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 ~flags:{Declarations.check_guarded=true} cofix;
+        check_cofix env ~flags:Declareops.safe_flags cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop c) ->
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index b84b1265e..6d84219d9 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -79,7 +79,7 @@ let adjust_guardness_conditions const = function
                     List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
                 env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
-                search_guard ~tflags:{Declarations.check_guarded=true} Loc.ghost env
+                search_guard ~tflags:Declareops.safe_flags Loc.ghost env
                   possible_indexes fixdecls in
 		(mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff) }
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6f2dd1bf1..ff43cd495 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -179,7 +179,7 @@ let declare_definition ~flags ident (local, p, k) ce pl imps hook =
   Lemmas.call_hook fix_exn hook local r
 
 let _ = Obligations.declare_definition_ref :=
-       (fun i k c imps hook -> declare_definition ~flags:{Declarations.check_guarded=true} i k c [] imps hook)
+       (fun i k c imps hook -> declare_definition ~flags:Declareops.safe_flags i k c [] imps hook)
 
 let do_definition ident k pl bl red_option c ctypopt hook =
   let (ce, evd, pl', imps as def) =
@@ -203,7 +203,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ~flags:{Declarations.check_guarded=true} ident k ce pl' imps
+      ignore(declare_definition ~flags:Declareops.safe_flags ident k ce pl' imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -838,7 +838,7 @@ let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),ef
   declare_definition ~flags f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref :=
-  (fun ?opaque k ctx f d t imps -> declare_fix ~flags:{Declarations.check_guarded=true} ?opaque k [] ctx f d t imps)
+  (fun ?opaque k ctx f d t imps -> declare_fix ~flags:Declareops.safe_flags ?opaque k [] ctx f d t imps)
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1269,11 +1269,11 @@ let do_program_recursive local p fixkind fixl ntns =
       in
       let indexes = 
         Pretyping.search_guard
-          ~tflags:{Declarations.check_guarded=true}
+          ~tflags:Declareops.safe_flags
           Loc.ghost (Global.env ()) possible_indexes fixdecls in
       List.iteri (fun i _ ->
           Inductive.check_fix env
-                              ~flags:{Declarations.check_guarded=true}
+                              ~flags:Declareops.safe_flags
                               ((indexes,i),fixdecls))
         fixl
   end in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 00fd97210..3d15f2142 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -567,7 +567,7 @@ let declare_mutual_definition l =
 	    List.map3 compute_possible_guardness_evidences
               wfl fixdefs fixtypes in
 	  let indexes = 
-              Pretyping.search_guard ~tflags:{Declarations.check_guarded=true}
+              Pretyping.search_guard ~tflags:Declareops.safe_flags
               Loc.ghost (Global.env())
               possible_indexes fixdecls in
           Some indexes, 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0b4dc0d18..5131a4179 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1731,7 +1731,7 @@ let vernac_load interp fname =
   try while true do interp (snd (parse_sentence input)) done
   with End_of_input -> ()
 
-let all_checks = { Declarations.check_guarded = true }
+let all_checks = Declareops.safe_flags
 
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands