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

This datatype does belong to this layer.

30 files changed, 71 insertions, 59 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 7fbad3ea96..68ae5628db 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -8,5 +8,5 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps
 
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-  edeclare ~name ~poly ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+  edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
     ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None []
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 9fed8b7829..57612c3735 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -12,10 +12,6 @@
 
 type discharge = DoDischarge | NoDischarge
 
-type import_status = ImportDefaultBehavior | ImportNeedQualified
-
-type locality = Discharge | Global of import_status
-
 type binding_kind = Explicit | Implicit
 
 type polymorphic = bool
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0d3c7b365f..a904b81d81 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -991,7 +991,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   in
   (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
   let info = Lemmas.Info.make
-      ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
       ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
 
   let lemma = Lemmas.start_lemma
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 65b114fc03..1f8bf5be22 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -387,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  save new_princ_name entry ~hook uctx Decl_kinds.(Global ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
+  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index b07a92658b..d305a58ccc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -418,7 +418,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
         ~program_mode:false
         ~name:fname
         ~poly:false
-        ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+        ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
         ~kind:Decl_kinds.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
@@ -436,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint ~scope:(Global ImportDefaultBehavior) ~poly:false fixpoint_exprl;
+       ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl;
        let evd,rev_pconstants =
          List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8745853180..254760cb50 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -118,8 +118,8 @@ let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
 (* Copy of the standard save mechanism but without the much too  *)
 (* slow reduction function                                       *)
 (*****************************************************************)
-open Decl_kinds
 open Declare
+open DeclareDef
 
 let definition_message = Declare.definition_message
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 602f7af57a..45d332031f 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -47,7 +47,7 @@ val save
   -> Evd.side_effects Proof_global.proof_entry
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
-  -> Decl_kinds.locality
+  -> DeclareDef.locality
   -> Decl_kinds.goal_object_kind
   -> unit
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 1ab64ac1b2..587e1fc2e8 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -804,7 +804,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let lem_id = mk_correct_id f_id in
          let (typ,_) = lemmas_types_infos.(i) in
          let info = Lemmas.Info.make
-             ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+             ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
              ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
          let lemma = Lemmas.start_lemma
              ~name:lem_id
@@ -870,7 +870,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
            i*)
          let lem_id = mk_complete_id f_id in
          let info = Lemmas.Info.make
-             ~scope:Decl_kinds.(Global ImportDefaultBehavior)
+             ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
              ~kind:Decl_kinds.(Proof Theorem) () in
          let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info
              sigma (fst lemmas_types_infos.(i)) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6663fa5c60..425e498330 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1368,7 +1368,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
   in
   let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
-      ~scope:Decl_kinds.(Global ImportDefaultBehavior) ~kind:Decl_kinds.(Proof Lemma)
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma)
       () in
   let lemma = Lemmas.start_lemma
       ~name:na
@@ -1411,7 +1411,7 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let info = Lemmas.Info.make ~hook ~scope:(Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
+    let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
     let lemma = Lemmas.start_lemma ~name:thm_name
         ~poly:false (*FIXME*)
         ~sign:(Environ.named_context_val env)
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 4ea5b676fb..465f736032 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -102,9 +102,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
      redundancy on constant declaration. This opens up an interesting
      question, how does abstract behave when discharge is local for example?
   *)
-  let scope, suffix = if opaque
-    then Global ImportDefaultBehavior, "_subproof"
-    else Global ImportDefaultBehavior, "_subterm" in
+  let suffix = if opaque
+    then "_subproof"
+    else "_subterm" in
   let name = name_op_to_name ~name_op ~name suffix in
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
@@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified name decl
+    Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:Declare.ImportNeedQualified name decl
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Proof_global.proof_entry_universes with
diff --git a/tactics/declare.ml b/tactics/declare.ml
index ca5d265733..02253e70bf 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -33,6 +33,8 @@ type internal_flag =
   | InternalTacticRequest  (* kernel action, no message is displayed *)
   | UserIndividualRequest   (* user action, a message is displayed *)
 
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 0a2332748c..bdb5af7430 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -51,6 +51,8 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   ?univs:Entries.universes_entry ->
   ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry
 
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
    the full path of the declaration
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