Merge PR coq#15233: Reduce explicit use of default definition scope

Reviewed-by: Alizter
Ack-by: gares
Co-authored-by: Alizter <[email protected]>

dev/ci/user-overlays/15233-SkySkimmer-locality.sh

@@ -0,0 +1 @@
+overlay equations https://github.com/SkySkimmer/Coq-Equations locality 15233

doc/plugin_tutorial/tuto1/src/simple_declare.ml

@@ -1,7 +1,4 @@
 let declare_definition ~poly name sigma body =
-  let udecl = UState.default_univ_decl in
-  let scope = Locality.Global Locality.ImportDefaultBehavior in
-  let kind = Decls.(IsDefinition Definition) in
   let cinfo = Declare.CInfo.make ~name ~typ:None () in
-  let info = Declare.Info.make ~scope ~kind  ~udecl ~poly () in
+  let info = Declare.Info.make ~poly () in
   Declare.declare_definition ~info ~cinfo ~opaque:false ~body sigma

plugins/funind/gen_principle.ml

@@ -320,7 +320,6 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
     let entry = Declare.definition_entry ~univs ?types body in
     let (_ : Names.GlobRef.t) =
       Declare.declare_entry ~name:new_princ_name ~hook
-        ~scope:(Locality.Global Locality.ImportDefaultBehavior)
         ~kind:Decls.(IsProof Theorem)
         ~impargs:[] ~uctx entry
     in
@@ -401,7 +400,6 @@ let register_struct is_rec fixpoint_exprl =
           Pp.(str "Body of Function must be given.")
     in
     ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
-      ~scope:(Locality.Global Locality.ImportDefaultBehavior)
       ~kind:Decls.Definition univs binders None body (Some rtype);
     let evd, rev_pconstants =
       List.fold_left
@@ -419,9 +417,7 @@ let register_struct is_rec fixpoint_exprl =
     in
     (None, evd, List.rev rev_pconstants)
   | _ ->
-    ComFixpoint.do_fixpoint
-      ~scope:(Locality.Global Locality.ImportDefaultBehavior) ~poly:false
-      fixpoint_exprl;
+    ComFixpoint.do_fixpoint ~poly:false fixpoint_exprl;
     let evd, rev_pconstants =
       List.fold_left
         (fun (evd, l) {Vernacexpr.fname} ->

plugins/ltac/rewrite.ml

@@ -1879,12 +1879,12 @@ let declare_projection name instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let types = Some (it_mkProd_or_LetIn typ ctx) in
-  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in
+  let kind = Decls.(IsDefinition Definition) in
   let impargs, udecl = [], UState.default_univ_decl in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
-  let info = Declare.Info.make ~scope ~kind ~udecl ~poly () in
+  let info = Declare.Info.make ~kind ~udecl ~poly () in
   let _r : GlobRef.t =
-    Declare.declare_definition ~cinfo ~info ~opaque ~body sigma
+    Declare.declare_definition ~cinfo ~info ~opaque:false ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
@@ -1948,7 +1948,7 @@ let add_morphism_as_parameter atts m n : unit =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let poly = atts.polymorphic in
-  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Locality.Global Locality.ImportDefaultBehavior in
+  let kind = Decls.(IsAssumption Logical) in
   let impargs, udecl = [], UState.default_univ_decl in
   let evd, types = build_morphism_signature env evd m in
   let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in

vernac/classes.ml

@@ -366,9 +366,8 @@ let instance_hook info global ?hook cst =
 
 let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
-  let scope = Locality.Global Locality.ImportDefaultBehavior in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:(Some termtype) () in
-  let info = Declare.Info.make ~kind ~scope ~poly ~udecl () in
+  let info = Declare.Info.make ~kind ~poly ~udecl () in
   let kn = Declare.declare_definition ~cinfo ~info ~opaque:false ~body:term sigma in
   instance_hook iinfo global ?hook kn
 
@@ -397,10 +396,9 @@ let declare_instance_program pm env sigma ~locality ~poly name pri impargs udecl
   let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in
   let hook = Declare.Hook.make hook in
   let uctx = Evd.evar_universe_context sigma in
-  let scope, kind = Locality.Global Locality.ImportDefaultBehavior,
-                    Decls.IsDefinition Decls.Instance in
+  let kind = Decls.IsDefinition Decls.Instance in
   let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
-  let info = Declare.Info.make  ~udecl ~scope ~poly ~kind ~hook () in
+  let info = Declare.Info.make  ~udecl ~poly ~kind ~hook () in
   let pm, _ =
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
   in pm

vernac/comAssumption.mli

@@ -26,7 +26,7 @@ val interp_assumption
 val do_assumptions
   :  program_mode:bool
   -> poly:bool
-  -> scope:Locality.locality
+  -> scope:Locality.definition_scope
   -> kind:Decls.assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list

vernac/comDefinition.ml

@@ -115,7 +115,7 @@ let definition_using env evd ~body ~types ~using =
   let terms = Option.List.cons types [body] in
   Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using
 
-let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
+let do_definition ?hook ~name ?scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = false in
   let env = Global.env() in
   let env = Environ.update_typing_flags ?typing_flags env in
@@ -127,7 +127,7 @@ let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl r
   let using = definition_using env evd ~body ~types ~using in
   let kind = Decls.IsDefinition kind in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
-  let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly ?typing_flags () in
+  let info = Declare.Info.make ?scope ~kind ?hook ~udecl ~poly ?typing_flags () in
   let _ : Names.GlobRef.t =
     Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
   in ()

vernac/comDefinition.mli

@@ -28,7 +28,7 @@ val interp_definition
 val do_definition
   :  ?hook:Declare.Hook.t
   -> name:Id.t
-  -> scope:Locality.locality
+  -> ?scope:Locality.definition_scope
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> kind:Decls.definition_object_kind
@@ -44,7 +44,7 @@ val do_definition_program
   :  ?hook:Declare.Hook.t
   -> pm:Declare.OblState.t
   -> name:Id.t
-  -> scope:Locality.locality
+  -> scope:Locality.definition_scope
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> kind:Decls.logical_kind

vernac/comFixpoint.ml

@@ -282,13 +282,13 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ?typing_flags ((f
   List.iter (Metasyntax.add_notation_interpretation ~local:(scope=Locality.Discharge) (Global.env())) ntns;
   lemma
 
-let declare_fixpoint_generic ?indexes ~scope ~poly ?typing_flags ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
+let declare_fixpoint_generic ?indexes ?scope ~poly ?typing_flags ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
   (* We shortcut the proof process *)
   let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
-  let info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl ?typing_flags () in
+  let info = Declare.Info.make ?scope ~kind:fix_kind ~poly ~udecl ?typing_flags () in
   let cinfo = fixitems in
   let _ : GlobRef.t list =
     Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx
@@ -333,9 +333,9 @@ let do_fixpoint_interactive ~scope ~poly ?typing_flags l : Declare.Proof.t =
   let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly ?typing_flags fix ntns in
   lemma
 
-let do_fixpoint ~scope ~poly ?typing_flags ?using l =
+let do_fixpoint ?scope ~poly ?typing_flags ?using l =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common ?typing_flags l in
-  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?typing_flags ?using fix ntns
+  declare_fixpoint_generic ~indexes:possible_indexes ?scope ~poly ?typing_flags ?using fix ntns
 
 let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
   let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in

vernac/comFixpoint.mli

@@ -16,25 +16,29 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive
-  : scope:Locality.locality
+  : scope:Locality.definition_scope
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> fixpoint_expr list
   -> Declare.Proof.t
 
 val do_fixpoint
-   : scope:Locality.locality
+   : ?scope:Locality.definition_scope
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> ?using:Vernacexpr.section_subset_expr
   -> fixpoint_expr list
   -> unit
 
 val do_cofixpoint_interactive :
-  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
+  scope:Locality.definition_scope -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
 
-val do_cofixpoint :
-  scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> cofixpoint_expr list -> unit
+val do_cofixpoint
+  : scope:Locality.definition_scope
+  -> poly:bool
+  -> ?using:Vernacexpr.section_subset_expr
+  -> cofixpoint_expr list
+  -> unit
 
 (************************************************************************)
 (** Internal API  *)

vernac/comProgramFixpoint.mli

@@ -13,7 +13,7 @@ open Vernacexpr
 (** Special Fixpoint handling when command is activated. *)
 val do_fixpoint :
      pm:Declare.OblState.t
-  -> scope:Locality.locality
+  -> scope:Locality.definition_scope
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> ?using:Vernacexpr.section_subset_expr
@@ -22,7 +22,7 @@ val do_fixpoint :
 
 val do_cofixpoint :
      pm:Declare.OblState.t
-  -> scope:Locality.locality
+  -> scope:Locality.definition_scope
   -> poly:bool
   -> ?using:Vernacexpr.section_subset_expr
   -> cofixpoint_expr list

vernac/declare.ml

@@ -26,7 +26,7 @@ module Hook = struct
       (** [(n1,t1),...(nm,tm)]: association list between obligation
           name and the corresponding defined term (might be a constant,
           but also an arbitrary term in the Expand case of obligations) *)
-      ; scope : Locality.locality
+      ; scope : Locality.definition_scope
       (**  [locality]: Locality of the original declaration *)
       ; dref : Names.GlobRef.t
       (** [ref]: identifier of the original declaration *)
@@ -81,15 +81,15 @@ module Info = struct
     ; inline : bool
     ; kind : Decls.logical_kind
     ; udecl : UState.universe_decl
-    ; scope : Locality.locality
+    ; scope : Locality.definition_scope
     ; hook : Hook.t option
     ; typing_flags : Declarations.typing_flags option
     }
 
   (** Note that [opaque] doesn't appear here as it is not known at the
      start of the proof in the interactive case. *)
   let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
-      ?(udecl=UState.default_univ_decl) ?(scope=Locality.Global Locality.ImportDefaultBehavior)
+      ?(udecl=UState.default_univ_decl) ?(scope=Locality.default_scope)
       ?hook ?typing_flags () =
     { poly; inline; kind; udecl; scope; hook; typing_flags }
 
@@ -651,7 +651,7 @@ let declare_definition_scheme ~internal ~univs ~role ~name c =
   kn, eff
 
 (* Locality stuff *)
-let declare_entry_core ~name ~scope ~kind ~typing_flags ?hook ~obls ~impargs ~uctx entry =
+let declare_entry_core ~name ?(scope=Locality.default_scope) ~kind ~typing_flags ?hook ~obls ~impargs ~uctx entry =
   let should_suggest =
     entry.proof_entry_opaque
     && not (List.is_empty (Global.named_context()))
@@ -2332,7 +2332,6 @@ let rec solve_obligation prg num tac =
     then Error.depends user_num remaining
   in
   let obl = subst_deps_obl obls obl in
-  let scope = Locality.Global Locality.ImportNeedQualified in
   let kind = kind_of_obligation (snd obl.obl_status) in
   let evd = Evd.from_ctx (Internal.get_uctx prg) in
   let evd = Evd.update_sigma_univs (Global.universes ()) evd in
@@ -2344,7 +2343,7 @@ let rec solve_obligation prg num tac =
   let using = Internal.get_using prg in
   let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) ?using () in
   let poly = Internal.get_poly prg in
-  let info = Info.make ~scope ~kind ~poly () in
+  let info = Info.make ~kind ~poly () in
   let lemma = Proof.start_core ~cinfo ~info ~proof_ending evd  in
   let lemma = fst @@ Proof.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Proof.set_endline_tactic tac lemma) lemma tac in
@@ -2584,5 +2583,5 @@ module OblState = Obls_.State
 let declare_constant ?local ~name ~kind ?typing_flags =
   declare_constant ?local ~name ~kind ~typing_flags
 
-let declare_entry ~name ~scope ~kind =
-  declare_entry ~name ~scope ~kind ~typing_flags:None
+let declare_entry ~name ?scope ~kind =
+  declare_entry ~name ?scope ~kind ~typing_flags:None

vernac/declare.mli

@@ -56,7 +56,7 @@ module Hook : sig
       (** [(n1,t1),...(nm,tm)]: association list between obligation
           name and the corresponding defined term (might be a constant,
           but also an arbitrary term in the Expand case of obligations) *)
-      ; scope : Locality.locality
+      ; scope : Locality.definition_scope
       (** [scope]: Locality of the original declaration *)
       ; dref : GlobRef.t
       (** [dref]: identifier of the original declaration *)
@@ -105,7 +105,7 @@ module Info : sig
     -> ?kind : Decls.logical_kind
     (** Theorem, etc... *)
     -> ?udecl : UState.universe_decl
-    -> ?scope : Locality.locality
+    -> ?scope : Locality.definition_scope
     (** locality  *)
     -> ?hook : Hook.t
     (** Callback to be executed after saving the constant *)
@@ -347,7 +347,7 @@ val primitive_entry
     instead *)
 val declare_entry
   :  name:Id.t
-  -> scope:Locality.locality
+  -> ?scope:Locality.definition_scope
   -> kind:Decls.logical_kind
   -> ?hook:Hook.t
   -> impargs:Impargs.manual_implicits

vernac/locality.ml

@@ -11,7 +11,9 @@
 (** * Managing locality *)
 
 type import_status = ImportDefaultBehavior | ImportNeedQualified
-type locality = Discharge | Global of import_status
+type definition_scope = Discharge | Global of import_status
+
+let default_scope = Global ImportDefaultBehavior
 
 let importability_of_bool = function
   | true -> ImportNeedQualified

vernac/locality.mli

@@ -11,7 +11,10 @@
 (** * Managing locality *)
 
 type import_status = ImportDefaultBehavior | ImportNeedQualified
-type locality = Discharge | Global of import_status
+type definition_scope = Discharge | Global of import_status
+
+val default_scope : definition_scope
+(** = [Global ImportDefaultBehavior] *)
 
 (** * Positioning locality for commands supporting discharging and export
     outside of modules *)
@@ -23,7 +26,7 @@ type locality = Discharge | Global of import_status
 
 val make_locality : bool option -> bool
 val make_non_locality : bool option -> bool
-val enforce_locality_exp : bool option -> Vernacexpr.discharge -> locality
+val enforce_locality_exp : bool option -> Vernacexpr.discharge -> definition_scope
 val enforce_locality : bool option -> bool
 
 (** For commands whose default is to not discharge but to export: