Factorizing the uses of Declareops.safe_flags.

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

2 files changed, 7 insertions, 7 deletions

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