[api] Move `locality` from `library` to `vernac`.

This datatype does belong to this layer.

18 files changed, 52 insertions, 40 deletions

diff --git a/vernac/class.ml b/vernac/class.ml
index d5c75ed809..9c22d24f93 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -356,6 +356,7 @@ let try_add_new_coercion_with_source ref ~local poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
 let add_coercion_hook poly _uctx _trans local ref =
+  let open DeclareDef in
   let local = match local with
   | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
@@ -368,6 +369,7 @@ let add_coercion_hook poly _uctx _trans local ref =
 let add_coercion_hook poly = DeclareDef.Hook.make (add_coercion_hook poly)
 
 let add_subclass_hook poly _uctx _trans local ref =
+  let open DeclareDef in
   let stre = match local with
   | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c8ae9928a3..98c71689f4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -363,7 +363,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
   let hook = DeclareDef.Hook.make hook in
   let ctx = Evd.evar_universe_context sigma in
   ignore(Obligations.add_definition ~name:id ?term:constr
-           ~univdecl:decl ~scope:(Global ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls)
+           ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls)
 
 let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
   (* spiwack: it is hard to reorder the actions to do
@@ -372,7 +372,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
      the refinement manually.*)
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
-  let scope = Decl_kinds.(Global ImportDefaultBehavior) in
+  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
   let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
   let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in
   let info = Lemmas.Info.make ~hook ~scope ~kind () in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index febe28879f..bf43438c1e 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -44,6 +44,7 @@ let should_axiom_into_instance = function
   | Definitional | Logical | Conjectural -> !axiom_into_instance
 
 let declare_assumption is_coe ~poly ~scope ~kind (c,ctx) pl imps impl nl {CAst.v=ident} =
+let open DeclareDef in
 match scope with
 | Discharge ->
   let ctx = match ctx with
@@ -123,6 +124,7 @@ let process_assumptions_udecls ~scope l =
       udecl, id
     | (_, ([], _))::_ | [] -> assert false
   in
+  let open DeclareDef in
   let () = match scope, udecl with
     | Discharge, Some _ ->
       let loc = first_id.CAst.loc in
@@ -289,14 +291,14 @@ let context poly l =
       in
       let impl = List.exists test impls in
       let scope =
-        if Lib.sections_are_opened () then Discharge else Global ImportDefaultBehavior in
+        if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in
       let nstatus = match b with
       | None ->
         pi3 (declare_assumption false ~scope ~poly ~kind:Context (t, univs) UnivNames.empty_binders [] impl
                Declaremods.NoInline (CAst.make id))
       | Some b ->
         let entry = Declare.definition_entry ~univs ~types:t b in
-        let _gr = DeclareDef.declare_definition ~name:id ~scope:Discharge ~kind:Definition UnivNames.empty_binders entry [] in
+        let _gr = DeclareDef.declare_definition ~name:id ~scope:DeclareDef.Discharge ~kind:Definition UnivNames.empty_binders entry [] in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
         status && nstatus
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 67fa94ceb8..4171c99836 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -18,7 +18,7 @@ open Decl_kinds
 val do_assumptions
   :  program_mode:bool
   -> poly:polymorphic
-  -> scope:locality
+  -> scope:DeclareDef.locality
   -> kind:assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
@@ -29,7 +29,7 @@ val do_assumptions
 val declare_assumption
   : coercion_flag
   -> poly:bool
-  -> scope:Decl_kinds.locality
+  -> scope:DeclareDef.locality
   -> kind:assumption_object_kind
   -> Constr.types Entries.in_universes_entry
   -> UnivNames.universe_binders
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index ec59916e3c..1058945668 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -19,7 +19,7 @@ val do_definition
   :  program_mode:bool
   -> ?hook:DeclareDef.Hook.t
   -> name:Id.t
-  -> scope:locality
+  -> scope:DeclareDef.locality
   -> poly:bool
   -> kind:definition_object_kind
   -> universe_decl_expr option
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index c04cc95837..982d316605 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Decl_kinds
 open Constrexpr
 open Vernacexpr
 
@@ -19,16 +18,16 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  scope:locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t
+  scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t
 
 val do_fixpoint :
-  scope:locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint_interactive :
-  scope:locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t
+  scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t
 
 val do_cofixpoint :
-  scope:locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index ba735f9c10..f25abb95c3 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -1,12 +1,11 @@
-open Decl_kinds
 open Vernacexpr
 
 (** Special Fixpoint handling when command is activated. *)
 
 val do_fixpoint :
   (* When [false], assume guarded. *)
-  scope:locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
   (* When [false], assume guarded. *)
-  scope:locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index e82fb3e3b1..d74fdcab2c 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -13,12 +13,14 @@ open Declare
 open Globnames
 open Impargs
 
+type locality = Discharge | Global of Declare.import_status
+
 (* Hooks naturally belong here as they apply to both definitions and lemmas *)
 module Hook = struct
   module S = struct
     type t = UState.t
       -> (Names.Id.t * Constr.t) list
-      -> Decl_kinds.locality
+      -> locality
       -> Names.GlobRef.t
       -> unit
   end
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 708158814e..75fd5dcf5b 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -11,6 +11,8 @@
 open Names
 open Decl_kinds
 
+type locality = Discharge | Global of Declare.import_status
+
 (** Declaration hooks *)
 module Hook : sig
   type t
@@ -28,7 +30,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) *)
-      -> Decl_kinds.locality
+      -> locality
       (**  [locality]: Locality of the original declaration *)
       -> GlobRef.t
       (** [ref]: identifier of the origianl declaration *)
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 1790932c23..81cde786c2 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -49,7 +49,7 @@ type program_info =
   ; prg_implicits : Impargs.manual_implicits
   ; prg_notations : notations
   ; prg_poly : bool
-  ; prg_scope : locality
+  ; prg_scope : DeclareDef.locality
   ; prg_kind : definition_object_kind
   ; prg_reduce : constr -> constr
   ; prg_hook : DeclareDef.Hook.t option
@@ -167,7 +167,7 @@ let declare_obligation prg obl body ty uctx =
     in
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
-      Declare.declare_constant obl.obl_name ~local:ImportNeedQualified
+      Declare.declare_constant obl.obl_name ~local:Declare.ImportNeedQualified
         (Declare.DefinitionEntry ce, IsProof Property)
     in
     if not opaque then
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 4774d73aa7..2d275b5ed8 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -43,7 +43,7 @@ type program_info =
   ; prg_implicits : Impargs.manual_implicits
   ; prg_notations : notations
   ; prg_poly : bool
-  ; prg_scope : Decl_kinds.locality
+  ; prg_scope : DeclareDef.locality
   ; prg_kind : Decl_kinds.definition_object_kind
   ; prg_reduce : constr -> constr
   ; prg_hook : DeclareDef.Hook.t option
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index aa3145bc5a..88a4491112 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -74,11 +74,11 @@ module Info = struct
     ; proof_ending : Proof_ending.t CEphemeron.key
     (* This could be improved and the CEphemeron removed *)
     ; other_thms : Recthm.t list
-    ; scope : Decl_kinds.locality
+    ; scope : DeclareDef.locality
     ; kind : Decl_kinds.goal_object_kind
     }
 
-  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Global ImportDefaultBehavior) ?(kind=Proof Lemma) () =
+  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Proof Lemma) () =
     { hook
     ; compute_guard = []
     ; impargs = []
@@ -246,7 +246,7 @@ let default_thm_id = Id.of_string "Unnamed_thm"
 let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
   if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
-     locality <> Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
+     locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
   then
     user_err ?loc  (Id.print id ++ str " already exists.")
 
@@ -256,6 +256,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
   let k = IsAssumption Conjectural in
   match body with
   | None ->
+    let open DeclareDef in
       (match scope with
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
@@ -284,6 +285,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
         | _ ->
           anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in
       let body_i = body_i body in
+      let open DeclareDef in
       match scope with
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
@@ -476,6 +478,7 @@ let get_keep_admitted_vars =
     ~value:true
 
 let finish_admitted env sigma id ~poly ~scope pe ctx hook ~udecl impargs other_thms =
+  let open DeclareDef in
   let local = match scope with
   | Global local -> local
   | Discharge -> warn_let_as_axiom id; ImportNeedQualified
@@ -558,6 +561,7 @@ let finish_proved env sigma opaque idopt po info =
       let const = adjust_guardness_conditions const compute_guard in
       let k = Kindops.logical_kind_of_goal_kind kind in
       let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
+      let open DeclareDef in
       let r = match scope with
         | Discharge ->
           let c = SectionLocalDef const in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a3df43f80e..88f26a04b7 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -85,7 +85,7 @@ module Info : sig
     (** Callback to be executed at the end of the proof *)
     -> ?proof_ending : Proof_ending.t
     (** Info for special constants *)
-    -> ?scope : Decl_kinds.locality
+    -> ?scope : DeclareDef.locality
     (** locality  *)
     -> ?kind:goal_object_kind
     (** Theorem, etc... *)
@@ -119,7 +119,7 @@ type lemma_possible_guards = int list list
 val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
   -> poly:bool
-  -> scope:locality
+  -> scope:DeclareDef.locality
   -> kind:goal_object_kind
   -> udecl:UState.universe_decl
   -> Evd.evar_map
@@ -134,7 +134,7 @@ val default_thm_id : Names.Id.t
 val start_lemma_com
   :  program_mode:bool
   -> poly:bool
-  -> scope:locality
+  -> scope:DeclareDef.locality
   -> kind:goal_object_kind
   -> ?inference_hook:Pretyping.inference_hook
   -> ?hook:DeclareDef.Hook.t
diff --git a/vernac/locality.ml b/vernac/locality.ml
index bc33d53594..2f703b675e 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -13,8 +13,8 @@ open Decl_kinds
 (** * Managing locality *)
 
 let importability_of_bool = function
-  | true -> ImportNeedQualified
-  | false -> ImportDefaultBehavior
+  | true -> Declare.ImportNeedQualified
+  | false -> Declare.ImportDefaultBehavior
 
 (** Positioning locality for commands supporting discharging and export
      outside of modules *)
@@ -36,13 +36,14 @@ let warn_local_declaration =
         strbrk "available without qualification when imported.")
 
 let enforce_locality_exp locality_flag discharge =
+  let open DeclareDef in
   match locality_flag, discharge with
   | Some b, NoDischarge -> Global (importability_of_bool b)
-  | None, NoDischarge -> Global ImportDefaultBehavior
+  | None, NoDischarge -> Global Declare.ImportDefaultBehavior
   | None, DoDischarge when not (Lib.sections_are_opened ()) ->
      (* If a Let/Variable is defined outside a section, then we consider it as a local definition *)
      warn_local_declaration ();
-     Global ImportNeedQualified
+     Global Declare.ImportNeedQualified
   | None, DoDischarge -> Discharge
   | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case")
   | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case")
diff --git a/vernac/locality.mli b/vernac/locality.mli
index be7e0cbe76..9c68b56a83 100644
--- a/vernac/locality.mli
+++ b/vernac/locality.mli
@@ -20,7 +20,7 @@
 
 val make_locality : bool option -> bool
 val make_non_locality : bool option -> bool
-val enforce_locality_exp : bool option -> Decl_kinds.discharge -> Decl_kinds.locality
+val enforce_locality_exp : bool option -> Decl_kinds.discharge -> DeclareDef.locality
 val enforce_locality : bool option -> bool
 
 (** For commands whose default is to not discharge but to export:
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ba514f9ab3..b7392a28ca 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -398,8 +398,8 @@ let deps_remaining obls deps =
     deps []
 
 
-let goal_kind = Decl_kinds.(Global ImportNeedQualified, DefinitionBody Definition)
-let goal_proof_kind = Decl_kinds.(Global ImportNeedQualified, Proof Lemma)
+let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, DefinitionBody Definition)
+let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Proof Lemma)
 
 let kind_of_obligation o =
   match o with
@@ -638,7 +638,7 @@ let show_term n =
             ++ Printer.pr_constr_env env sigma prg.prg_body)
 
 let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
-                   ?(implicits=[]) ~poly ?(scope=Global ImportDefaultBehavior) ?(kind=Definition) ?tactic
+                   ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?tactic
     ?(reduce=reduce) ?hook ?(opaque = false) obls =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let info = Id.print name ++ str " has type-checked" in
@@ -658,7 +658,7 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
-                           ~poly ?(scope=Global ImportDefaultBehavior) ?(kind=Definition) ?(reduce=reduce)
+                           ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?(reduce=reduce)
     ?hook ?(opaque = false) notations fixkind =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
@@ -689,7 +689,7 @@ let admit_prog prg =
         | None ->
             let x = subst_deps_obl obls x in
             let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
-            let kn = Declare.declare_constant x.obl_name ~local:ImportNeedQualified
+            let kn = Declare.declare_constant x.obl_name ~local:Declare.ImportNeedQualified
               (Declare.ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 787ab53e66..233739ee46 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -49,7 +49,7 @@ val add_definition
   -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
   -> ?implicits:Impargs.manual_implicits
   -> poly:bool
-  -> ?scope:Decl_kinds.locality
+  -> ?scope:DeclareDef.locality
   -> ?kind:Decl_kinds.definition_object_kind
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(constr -> constr)
@@ -65,7 +65,7 @@ val add_mutual_definitions
   (** Universe binders and constraints *)
   -> ?tactic:unit Proofview.tactic
   -> poly:bool
-  -> ?scope:Decl_kinds.locality
+  -> ?scope:DeclareDef.locality
   -> ?kind:Decl_kinds.definition_object_kind
   -> ?reduce:(constr -> constr)
   -> ?hook:DeclareDef.Hook.t -> ?opaque:bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ee00bc0e2a..697dca788d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -603,6 +603,7 @@ let vernac_definition_name lid local =
          CAst.make ?loc (fresh_name_for_anonymous_theorem ())
     | { v = Name.Name n; loc } -> CAst.make ?loc n in
   let () =
+    let open DeclareDef in
     match local with
     | Discharge -> Dumpglob.dump_definition lid true "var"
     | Global _ -> Dumpglob.dump_definition lid false "def"
@@ -671,8 +672,8 @@ let vernac_assumption ~atts discharge kind l nl =
     if Dumpglob.dump () then
       List.iter (fun (lid, _) ->
           match scope with
-            | Global _ -> Dumpglob.dump_definition lid false "ax"
-            | Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
+            | DeclareDef.Global _ -> Dumpglob.dump_definition lid false "ax"
+            | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
   let status = ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom