Moving the typing_flags to the environment.

4 files changed, 17 insertions, 17 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 335263f8f..4e9e68dff 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:Declareops.safe_flags ((id,ty,poly),ctx) in
+      let () = Global.push_named_assum ((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:Declareops.safe_flags (id,de) in
+      let univs = Global.push_named_def (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), Declareops.safe_flags)
+    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
@@ -205,7 +205,7 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
 let declare_scheme = ref (fun _ _ -> assert false)
 let set_declare_scheme f = declare_scheme := f
 
-let declare_constant_common ~flags id cst =
+let declare_constant_common id cst =
   let update_tables c =
 (*  Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *)
     declare_constant_implicits c;
@@ -216,7 +216,7 @@ let declare_constant_common ~flags id cst =
   List.iter (fun (c,ce,role) ->
       (* handling of private_constants just exported *)
       let o = inConstant {
-        cst_decl = ConstantEntry (false, ce, flags);
+        cst_decl = ConstantEntry (false, ce);
         cst_hyps = [] ;
         cst_kind = IsProof Theorem;
         cst_locl = false;
@@ -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=Declareops.safe_flags) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let export = (* We deal with side effects *)
     match cd with
     | DefinitionEntry de when
@@ -259,24 +259,24 @@ let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualR
     | _ -> false
   in
   let cst = {
-    cst_decl = ConstantEntry (export,cd,flags);
+    cst_decl = ConstantEntry (export,cd);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
     cst_exported = [];
     cst_was_seff = false;
   } in
-  let kn = declare_constant_common id cst ~flags in
+  let kn = declare_constant_common id cst in
   let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
   kn
 
-let declare_definition ?flags ?(internal=UserIndividualRequest)
+let declare_definition ?(internal=UserIndividualRequest)
   ?(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 ?flags ~internal ~local id
+    declare_constant ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of inductive blocks *)
@@ -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:Declareops.safe_flags id (ProjectionEntry entry,
+	let kn' = declare_constant 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 41221d5c9..8dd24d278 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -54,11 +54,9 @@ 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 Declareops.safe_flags *)
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
-  ?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/library/global.ml b/library/global.ml
index e456841f8..c53611931 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,13 +77,14 @@ let globalize_with_summary fs f =
 
 let i2l = Label.of_id
 
-let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a)
-let push_named_def ~flags d = globalize (Safe_typing.push_named_def ~flags d)
+let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
+let push_named_def d = globalize (Safe_typing.push_named_def d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 let push_context b c = globalize0 (Safe_typing.push_context b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
+let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index 91fc55918..247ca20b4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,11 +27,12 @@ val named_context : unit -> Context.Named.t
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
+val set_typing_flags : Declarations.typing_flags -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : flags:Declarations.typing_flags -> (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def   : flags:Declarations.typing_flags -> (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
+val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
+val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
 
 val add_constant :
   DirPath.t -> Id.t -> Safe_typing.global_declaration ->