Remove [in_section] arguments to Safe_typing functions

The information is already there.

At some point we may want to clean up the Lib API to reduce redundancy
wrt kernel functions like [sections_are_opened], but I'm not doing now
as it would conflict with https://github.com/coq/coq/pull/10670

5 files changed, 24 insertions, 19 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9b4d2e69ac..fc55720583 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -173,6 +173,8 @@ let is_initial senv =
   | [], NONE -> ModPath.equal senv.modpath ModPath.initial
   | _ -> false
 
+let sections_are_opened senv = not (Section.is_empty senv.sections)
+
 let delta_of_senv senv = senv.modresolver,senv.paramresolver
 
 let constant_of_delta_kn_senv senv kn =
@@ -587,10 +589,10 @@ type global_declaration =
 
 type exported_private_constant = Constant.t
 
-let add_constant_aux ~in_section senv (kn, cb) =
+let add_constant_aux senv (kn, cb) =
   let l = Constant.label kn in
   (* This is the only place where we hashcons the contents of a constant body *)
-  let cb = if in_section then cb else Declareops.hcons_const_body cb in
+  let cb = if sections_are_opened senv then cb else Declareops.hcons_const_body cb in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
@@ -799,7 +801,7 @@ let push_opaque_proof pf senv =
   let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
   senv, o
 
-let export_private_constants ~in_section ce senv =
+let export_private_constants ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
   let map senv (kn, c) = match c.const_body with
   | OpaqueDef p ->
@@ -815,10 +817,10 @@ let export_private_constants ~in_section ce senv =
   let senv, bodies = List.fold_left_map map senv exported in
   let exported = List.map (fun (kn, _) -> kn) exported in
   (* No delayed constants to declare *)
-  let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
+  let senv = List.fold_left add_constant_aux senv bodies in
   (ce, exported), senv
 
-let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment =
+let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constant.t * a) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
     let cb = 
       match decl with
@@ -852,14 +854,14 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
     | Undef _ | Def _ | Primitive _ as body ->
       senv, { cb with const_body = body }, []
     in
-    let senv = add_constant_aux ~in_section senv (kn, cb) in
+    let senv = add_constant_aux senv (kn, cb) in
     add_constraints_list delayed_cst senv
   in
 
   let senv =
     match decl with
     | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) ->
-      if in_section then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
+      if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
@@ -1001,12 +1003,11 @@ let close_section senv =
   in
   let fold senv = function
   | `Definition (kn, cb) ->
-    let in_section = not (Section.is_empty senv.sections) in
     let info = cooking_info (Section.segment_of_constant env0 kn sections0) in
     let r = { Cooking.from = cb; info } in
     let cb = Term_typing.translate_recipe senv.env kn r in
     (* Delayed constants are already in the global environment *)
-    add_constant_aux ~in_section senv (kn, cb)
+    add_constant_aux senv (kn, cb)
   | `Inductive (ind, mib) ->
     let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
     let mie = Cooking.cook_inductive info mib in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index d97d61a72f..1b55293f1c 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -82,13 +82,13 @@ type global_declaration =
 
 type exported_private_constant = Constant.t
 
-val export_private_constants : in_section:bool ->
+val export_private_constants :
   private_constants Entries.proof_output ->
   (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
 
 (** returns the main constant plus a certificate of its validity *)
 val add_constant :
-  side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration ->
+  side_effect:'a effect_entry -> Label.t -> global_declaration ->
     (Constant.t * 'a) safe_transformer
 
 (** Adding an inductive type *)
@@ -138,6 +138,8 @@ val open_section : safe_transformer0
 
 val close_section : safe_transformer0
 
+val sections_are_opened : safe_environment -> bool
+
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
diff --git a/library/global.ml b/library/global.ml
index c4685370d1..24cfc57f28 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -102,8 +102,8 @@ let typing_flags () = Environ.typing_flags (env ())
 let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
-let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
-let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d)
+let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
+let add_constant ~side_effect id d = globalize (Safe_typing.add_constant ~side_effect (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
@@ -111,6 +111,7 @@ let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
 
 let open_section () = globalize0 Safe_typing.open_section
 let close_section fs = globalize0_with_summary fs Safe_typing.close_section
+let sections_are_opened () = Safe_typing.sections_are_opened (safe_env())
 
 let start_module id = globalize (Safe_typing.start_module (i2l id))
 let start_modtype id = globalize (Safe_typing.start_modtype (i2l id))
diff --git a/library/global.mli b/library/global.mli
index c45bf65d84..d689771f0a 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,12 +46,12 @@ val push_named_assum : (Id.t * Constr.types) -> unit
 val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
 val push_section_context : (Name.t array * Univ.UContext.t) -> unit
 
-val export_private_constants : in_section:bool ->
+val export_private_constants :
   Safe_typing.private_constants Entries.proof_output ->
   Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
 
 val add_constant :
-  side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
+  side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a
 val add_mind :
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
@@ -80,6 +80,8 @@ val close_section : Summary.frozen -> unit
 (** Close the section and reset the global state to the one at the time when
     the section what opened. *)
 
+val sections_are_opened : unit -> bool
+
 (** Interactive modules and module types *)
 
 val start_module : Id.t -> ModPath.t
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 3590146dfb..c7c0766587 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -249,14 +249,13 @@ let is_unsafe_typing_flags () =
 
 let define_constant ~side_effect ~name cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
-  let in_section = Lib.sections_are_opened () in
   let export, decl, unsafe = match cd with
   | DefinitionEntry de ->
     (* We deal with side effects *)
     if not de.proof_entry_opaque then
       (* This globally defines the side-effects in the environment. *)
       let body, eff = Future.force de.proof_entry_body in
-      let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in
+      let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in
       let export = get_roles export eff in
       let de = { de with proof_entry_body = Future.from_val (body, ()) } in
       let cd = Entries.DefinitionEntry (cast_proof_entry de) in
@@ -272,7 +271,7 @@ let define_constant ~side_effect ~name cd =
   | PrimitiveEntry e ->
     [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false
   in
-  let kn, eff = Global.add_constant ~side_effect ~in_section name decl in
+  let kn, eff = Global.add_constant ~side_effect name decl in
   if unsafe || is_unsafe_typing_flags() then feedback_axiom();
   kn, eff, export
 
@@ -319,7 +318,7 @@ let declare_variable ~name ~kind d =
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
       let (body, eff) = Future.force de.proof_entry_body in
-      let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
+      let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in
       let eff = get_roles export eff in
       let () = List.iter register_side_effect eff in
       let poly, univs = match de.proof_entry_universes with