[declare] [api] Removal of duplicated type aliases.

22 files changed, 94 insertions, 104 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 5431a21b53..73292e0120 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,6 +1,6 @@
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-  let scope = Declare.Global Declare.ImportDefaultBehavior in
+  let scope = Locality.Global Locality.ImportDefaultBehavior in
   let kind = Decls.(IsDefinition Definition) in
   let info = Declare.CInfo.make ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly () in
   Declare.declare_definition ~name ~info ~types:None ~body sigma
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c0d7c1e8e6..6ec12db952 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -860,7 +860,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   in
   let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
   let () =
-    Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
+    Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
       ~idopt:None
   in
   evd
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 30069c9914..8a07c2109e 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -319,7 +319,7 @@ 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:(Declare.Global Declare.ImportDefaultBehavior)
+        ~scope:(Locality.Global Locality.ImportDefaultBehavior)
         ~kind:Decls.(IsProof Theorem)
         ~impargs:[] ~uctx entry
     in
@@ -400,7 +400,7 @@ 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:(Declare.Global Declare.ImportDefaultBehavior)
+      ~scope:(Locality.Global Locality.ImportDefaultBehavior)
       ~kind:Decls.Definition univs binders None body (Some rtype);
     let evd, rev_pconstants =
       List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
     (None, evd, List.rev rev_pconstants)
   | _ ->
     ComFixpoint.do_fixpoint
-      ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
+      ~scope:(Locality.Global Locality.ImportDefaultBehavior) ~poly:false
       fixpoint_exprl;
     let evd, rev_pconstants =
       List.fold_left
@@ -1370,12 +1370,12 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
       | None -> raise Not_found
       | Some finfos -> finfos
     in
-    let open Declare in
     match finfos.equation_lemma with
-    | None -> Transparent (* non recursive definition *)
+    | None -> Vernacexpr.Transparent (* non recursive definition *)
     | Some equation ->
-      if Declareops.is_opaque (Global.lookup_constant equation) then Opaque
-      else Transparent
+      if Declareops.is_opaque (Global.lookup_constant equation) then
+        Vernacexpr.Opaque
+      else Vernacexpr.Transparent
   in
   let body, typ, univs, _hook, sigma0 =
     try
@@ -1527,8 +1527,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
             fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
-              ~idopt:None
+            Declare.save_lemma_proved ~proof:lemma
+              ~opaque:Vernacexpr.Transparent ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
@@ -1600,8 +1600,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                  lemma)
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
-              ~idopt:None
+            Declare.save_lemma_proved ~proof:lemma
+              ~opaque:Vernacexpr.Transparent ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
@@ -2205,7 +2205,7 @@ let build_scheme fas =
   List.iter2
     (fun (princ_id, _, _) (body, types, univs, opaque) ->
       let (_ : Constant.t) =
-        let opaque = if opaque = Declare.Opaque then true else false in
+        let opaque = if opaque = Vernacexpr.Opaque then true else false in
         let def_entry = Declare.definition_entry ~univs ~opaque ?types body in
         Declare.declare_constant ~name:princ_id
           ~kind:Decls.(IsProof Theorem)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 58ed3864bb..853a54592d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,7 +58,8 @@ let declare_fun name kind ?univs value =
     (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent ~idopt:None
+  Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
+    ~idopt:None
 
 let def_of_const t =
   match Constr.kind t with
@@ -1414,11 +1415,12 @@ let build_new_goal_type lemma =
 
 let is_opaque_constant c =
   let cb = Global.lookup_constant c in
+  let open Vernacexpr in
   match cb.Declarations.const_body with
-  | Declarations.OpaqueDef _ -> Declare.Opaque
-  | Declarations.Undef _ -> Declare.Opaque
-  | Declarations.Def _ -> Declare.Transparent
-  | Declarations.Primitive _ -> Declare.Opaque
+  | Declarations.OpaqueDef _ -> Opaque
+  | Declarations.Undef _ -> Opaque
+  | Declarations.Def _ -> Transparent
+  | Declarations.Primitive _ -> Opaque
 
 let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     (gls_type, decompose_and_tac, nb_goal) =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 67d09acfda..0bf97fefa6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1900,7 +1900,7 @@ 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, Declare.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in
   let _r : GlobRef.t =
@@ -1968,7 +1968,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, Declare.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Locality.Global Locality.ImportDefaultBehavior 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
diff --git a/stm/stm.ml b/stm/stm.ml
index 7aaa359149..800115ce42 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1523,7 +1523,7 @@ end = struct (* {{{ *)
             PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
-          let opaque = Declare.Opaque in
+          let opaque = Opaque in
           try
             let _pstate =
               stm_qed_delay_proof ~st ~id:stop
@@ -1667,7 +1667,7 @@ end = struct (* {{{ *)
         let _proof = PG_compat.return_partial_proof () in
         `OK_ADMITTED
       else begin
-      let opaque = Declare.Opaque in
+      let opaque = Opaque in
 
       (* The original terminator, a hook, has not been saved in the .vio*)
       let proof, _info =
@@ -2162,7 +2162,7 @@ let collect_proof keep cur hd brkind id =
    | id :: _ -> Names.Id.to_string id in
  let loc = (snd cur).expr.CAst.loc in
  let is_defined_expr = function
-   | VernacEndProof (Proved (Declare.Transparent,_)) -> true
+   | VernacEndProof (Proved (Transparent,_)) -> true
    | _ -> false in
  let is_defined = function
    | _, { expr = e } -> is_defined_expr e.CAst.v.expr
@@ -2527,7 +2527,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                   | VtKeep VtKeepAxiom ->
                       qed.fproof <- Some (None, ref false); None
                   | VtKeep opaque ->
-                    let opaque = let open Declare in  match opaque with
+                    let opaque = match opaque with
                       | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
                       | VtKeepAxiom -> assert false
                     in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index cf127648b4..a957f7354f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -37,7 +37,7 @@ let string_of_vernac_classification = function
   | VtMeta -> "Meta "
   | VtProofMode _ -> "Proof Mode"
 
-let vtkeep_of_opaque = let open Declare in function
+let vtkeep_of_opaque = function
   | Opaque -> VtKeepOpaque
   | Transparent -> VtKeepDefined
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c4c6a0fa33..b36a6fa3a6 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -313,7 +313,7 @@ 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 = Declare.Global Declare.ImportDefaultBehavior in
+  let scope = Locality.Global Locality.ImportDefaultBehavior in
   let info = Declare.CInfo.make ~kind ~scope ~impargs ~opaque:false ~poly ~udecl () in
   let kn = Declare.declare_definition ~name ~info ~types:(Some termtype) ~body:term sigma in
   instance_hook iinfo global ?hook kn
@@ -344,7 +344,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term
   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 = Declare.Global Declare.ImportDefaultBehavior,
+  let scope, kind = Locality.Global Locality.ImportDefaultBehavior,
                     Decls.IsDefinition Decls.Instance in
   let _ : Declare.progress =
     Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 9c82eb8960..d8475126ca 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -61,8 +61,8 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
   let sigma = Evd.from_env env in
   let () = if do_instance then Classes.declare_instance env sigma None false gr in
   let local = match local with
-    | Declare.ImportNeedQualified -> true
-    | Declare.ImportDefaultBehavior -> false
+    | Locality.ImportNeedQualified -> true
+    | Locality.ImportDefaultBehavior -> false
   in
   let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in
   let inst = instance_of_univ_entry univs in
@@ -86,11 +86,11 @@ let context_set_of_entry = function
   | Monomorphic_entry uctx -> uctx
 
 let declare_assumptions ~poly ~scope ~kind univs nl l =
-  let () = let open Declare in match scope with
-    | Discharge ->
+  let () = match scope with
+    | Locality.Discharge ->
       (* declare universes separately for variables *)
       DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs))
-    | Global _ -> ()
+    | Locality.Global _ -> ()
   in
   let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) ->
       (* NB: here univs are ignored when scope=Discharge *)
@@ -98,10 +98,10 @@ let declare_assumptions ~poly ~scope ~kind univs nl l =
       let univs,subst' =
         List.fold_left_map (fun univs id ->
             let refu = match scope with
-              | Declare.Discharge ->
+              | Locality.Discharge ->
                 declare_variable is_coe ~kind typ imps Glob_term.Explicit id;
                 GlobRef.VarRef id.CAst.v, Univ.Instance.empty
-              | Declare.Global local ->
+              | Locality.Global local ->
                 declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id
             in
             next_univs univs, (id.CAst.v, Constr.mkRef refu))
@@ -128,9 +128,8 @@ let process_assumptions_udecls ~scope l =
       udecl, id
     | (_, ([], _))::_ | [] -> assert false
   in
-  let open Declare in
   let () = match scope, udecl with
-    | Discharge, Some _ ->
+    | Locality.Discharge, Some _ ->
       let loc = first_id.CAst.loc in
       let msg = Pp.str "Section variables cannot be polymorphic." in
       user_err ?loc  msg
@@ -206,7 +205,7 @@ let context_insection sigma ~poly ctx =
         let uctx = Evd.evar_universe_context sigma in
         let kind = Decls.(IsDefinition Definition) in
         let _ : GlobRef.t =
-          Declare.declare_entry ~name ~scope:Declare.Discharge
+          Declare.declare_entry ~name ~scope:Locality.Discharge
             ~kind ~impargs:[] ~uctx entry
         in
         ()
@@ -237,8 +236,8 @@ let context_nosection sigma ~poly ctx =
         let entry = Declare.definition_entry ~univs ~types:t b in
         Declare.DefinitionEntry entry
     in
-    let local = if Lib.is_modtype () then Declare.ImportDefaultBehavior
-      else Declare.ImportNeedQualified
+    let local = if Lib.is_modtype () then Locality.ImportDefaultBehavior
+      else Locality.ImportNeedQualified
     in
     let cst = Declare.declare_constant ~name ~kind ~local decl in
     let () = Declare.assumption_message name in
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 989015a9f3..3d425ad768 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -17,7 +17,7 @@ open Constrexpr
 val do_assumptions
   :  program_mode:bool
   -> poly:bool
-  -> scope:Declare.locality
+  -> scope:Locality.locality
   -> kind:Decls.assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
@@ -35,7 +35,7 @@ val declare_variable
 val declare_axiom
   : coercion_flag
   -> poly:bool
-  -> local:Declare.import_status
+  -> local:Locality.import_status
   -> kind:Decls.assumption_object_kind
   -> Constr.types
   -> Entries.universes_entry * UnivNames.universe_binders
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 3cc5dd65af..15d8ebc4b5 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -354,7 +354,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 { Declare.Hook.S.scope; dref; _ } =
-  let open Declare in
+  let open Locality in
   let local = match scope with
   | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
@@ -367,7 +367,7 @@ let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } =
 let add_coercion_hook ~poly = Declare.Hook.make (add_coercion_hook poly)
 
 let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } =
-  let open Declare in
+  let open Locality in
   let stre = match scope with
   | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 2b846f17e0..e3417d0062 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -17,7 +17,7 @@ open Constrexpr
 val do_definition
   :  ?hook:Declare.Hook.t
   -> name:Id.t
-  -> scope:Declare.locality
+  -> scope:Locality.locality
   -> poly:bool
   -> kind:Decls.definition_object_kind
   -> universe_decl_expr option
@@ -30,7 +30,7 @@ val do_definition
 val do_definition_program
   :  ?hook:Declare.Hook.t
   -> name:Id.t
-  -> scope:Declare.locality
+  -> scope:Locality.locality
   -> poly:bool
   -> kind:Decls.logical_kind
   -> universe_decl_expr option
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 486d0156f9..aa5446205c 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -16,16 +16,16 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
+  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
 
 val do_fixpoint :
-  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
+  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
 
 val do_cofixpoint :
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index ec37ec7fa8..b05bf9a675 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -56,7 +56,7 @@ let project_hint ~poly pri l2r r =
     Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c))
   in
   let c =
-    Declare.declare_constant ~local:Declare.ImportDefaultBehavior ~name
+    Declare.declare_constant ~local:Locality.ImportDefaultBehavior ~name
       ~kind:Decls.(IsDefinition Definition)
       cb
   in
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 8b1fa6c202..e39f62c348 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -14,8 +14,8 @@ open Vernacexpr
 
 val do_fixpoint :
   (* When [false], assume guarded. *)
-  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint :
   (* When [false], assume guarded. *)
-  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
+  scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit
diff --git a/vernac/declare.ml b/vernac/declare.ml
index fde332cb66..430639b637 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -16,8 +16,6 @@ open Names
 open Safe_typing
 module NamedDecl = Context.Named.Declaration
 
-type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent
-
 (* Hooks naturally belong here as they apply to both definitions and lemmas *)
 module Hook = struct
   module S = struct
@@ -284,8 +282,6 @@ let get_open_goals ps =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
   List.length shelf
 
-type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified
-
 (** Declaration of constants and parameters *)
 
 type 'a proof_entry = {
@@ -409,7 +405,9 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
   let { Proof.name; poly } = Proof.data proof in
   let unsafe_typ = keep_body_ucst_separate && not poly in
   let elist, uctx = prepare_proof ~unsafe_typ ps in
-  let opaque = match opaque with Opaque -> true | Transparent -> false in
+  let opaque = match opaque with
+    | Vernacexpr.Opaque -> true
+    | Vernacexpr.Transparent -> false in
 
   let make_entry ((((_ub, body) as b), eff), ((_ut, typ) as t)) =
     let utyp, ubody =
@@ -435,7 +433,7 @@ type 'a constant_entry =
 
 type constant_obj = {
   cst_kind : Decls.logical_kind;
-  cst_locl : import_status;
+  cst_locl : Locality.import_status;
 }
 
 let load_constant i ((sp,kn), obj) =
@@ -449,8 +447,8 @@ let load_constant i ((sp,kn), obj) =
 let open_constant f i ((sp,kn), obj) =
   (* Never open a local definition *)
   match obj.cst_locl with
-  | ImportNeedQualified -> ()
-  | ImportDefaultBehavior ->
+  | Locality.ImportNeedQualified -> ()
+  | Locality.ImportDefaultBehavior ->
     let con = Global.constant_of_delta_kn kn in
     if Libobject.in_filter_ref (GlobRef.ConstRef con) f then
       Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
@@ -504,7 +502,7 @@ let register_constant kn kind local =
   update_tables kn
 
 let register_side_effect (c, role) =
-  let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in
+  let () = register_constant c Decls.(IsProof Theorem) Locality.ImportDefaultBehavior in
   match role with
   | None -> ()
   | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|]
@@ -661,14 +659,14 @@ let define_constant ~name cd =
   if unsafe || is_unsafe_typing_flags() then feedback_axiom();
   kn
 
-let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
+let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind cd =
   let () = check_exists name in
   let kn = define_constant ~name cd in
   (* Register the libobjects attached to the constants *)
   let () = register_constant kn kind local in
   kn
 
-let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de =
+let declare_private_constant ?role ?(local = Locality.ImportDefaultBehavior) ~name ~kind de =
   let kn, eff =
     let de =
       if not de.proof_entry_opaque then
@@ -921,7 +919,7 @@ let next = let n = ref 0 in fun () -> incr n; !n
 
 let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac)
 
-let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac =
+let build_constant_by_tactic ~name ?(opaque=Vernacexpr.Transparent) ~uctx ~sign ~poly typ tac =
   let evd = Evd.from_ctx uctx in
   let info = Info.make () in
   let pf = start_proof_core ~name ~poly ~sign ~udecl:UState.default_univ_decl ~impargs:[] ~info evd typ in
@@ -962,7 +960,7 @@ let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma c
   let concl = EConstr.of_constr concl in
   let uctx = Evd.evar_universe_context sigma in
   let (const, safe, uctx) =
-    try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx ~sign:secsign concl solve_tac
+    try build_constant_by_tactic ~name ~opaque:Vernacexpr.Transparent ~poly ~uctx ~sign:secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
@@ -986,7 +984,7 @@ let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma c
     (* 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_private_constant ~local:ImportNeedQualified ~name ~kind const
+    declare_private_constant ~local:Locality.ImportNeedQualified ~name ~kind const
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.proof_entry_universes with
@@ -1033,8 +1031,6 @@ let declare_definition_scheme ~internal ~univs ~role ~name c =
 let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
 let _ = Abstract.declare_abstract := declare_abstract
 
-type locality = Locality.locality = | Discharge | Global of import_status
-
 module CInfo = struct
 
   type t =
@@ -1043,13 +1039,13 @@ module CInfo = struct
     ; inline : bool
     ; kind : Decls.logical_kind
     ; udecl : UState.universe_decl
-    ; scope : locality
+    ; scope : Locality.locality
     ; impargs : Impargs.manual_implicits
     ; hook : Hook.t option
     }
 
   let make ?(poly=false) ?(opaque=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
-      ?(udecl=UState.default_univ_decl) ?(scope=Global ImportNeedQualified) ?(impargs=[])
+      ?(udecl=UState.default_univ_decl) ?(scope=Locality.Global Locality.ImportNeedQualified) ?(impargs=[])
       ?hook () =
     { poly; opaque; inline; kind; udecl; scope; impargs; hook }
 
@@ -1064,11 +1060,11 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
   in
   let ubind = UState.universe_binders uctx in
   let dref = match scope with
-  | Discharge ->
+  | Locality.Discharge ->
     let () = declare_variable_core ~name ~kind (SectionLocalDef entry) in
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
-  | Global local ->
+  | Locality.Global local ->
     let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in
     let gr = Names.GlobRef.ConstRef kn in
     if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
@@ -1131,8 +1127,8 @@ let warn_let_as_axiom =
 
 let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
   let local = match scope with
-    | Discharge -> warn_let_as_axiom name; ImportNeedQualified
-    | Global local -> local
+    | Locality.Discharge -> warn_let_as_axiom name; Locality.ImportNeedQualified
+    | Locality.Global local -> local
   in
   let kind = Decls.(IsAssumption Conjectural) in
   let decl = ParameterEntry pe in
@@ -1390,7 +1386,7 @@ let declare_obligation prg obl ~uctx ~types ~body =
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       declare_constant ~name:obl.obl_name
-        ~local:ImportNeedQualified
+        ~local:Locality.ImportNeedQualified
         ~kind:Decls.(IsProof Property)
         (DefinitionEntry ce)
     in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 002328b63f..67389d2966 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -162,8 +162,6 @@ module Proof : sig
   val info : t -> Info.t
 end
 
-type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent
-
 (** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
    name [name] with goals [goals] (a list of pairs of environment and
    conclusion); [poly] determines if the proof is universe
@@ -219,7 +217,7 @@ type proof_object
 (** Used by the STM only to store info, should go away *)
 val get_po_name : proof_object -> Id.t
 
-val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object
+val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object
 
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
@@ -252,8 +250,6 @@ val definition_entry
   -> constr
   -> Evd.side_effects proof_entry
 
-type import_status = Locality.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
@@ -265,7 +261,7 @@ type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeed
   for removal from the public API, use higher-level declare APIs
   instead *)
 val declare_constant
-  :  ?local:import_status
+  :  ?local:Locality.import_status
   -> name:Id.t
   -> kind:Decls.logical_kind
   -> Evd.side_effects constant_entry
@@ -337,8 +333,6 @@ val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env
   environment and empty evar_map. *)
 val get_current_context : Proof.t -> Evd.evar_map * Environ.env
 
-type locality = Locality.locality = Discharge | Global of import_status
-
 (** Information for a constant *)
 module CInfo : sig
 
@@ -351,7 +345,7 @@ module CInfo : sig
     -> ?kind : Decls.logical_kind
     (** Theorem, etc... *)
     -> ?udecl : UState.universe_decl
-    -> ?scope : locality
+    -> ?scope : Locality.locality
     (** locality  *)
     -> ?impargs : Impargs.manual_implicits
     -> ?hook : Hook.t
@@ -366,7 +360,7 @@ end
     instead *)
 val declare_entry
   :  name:Id.t
-  -> scope:locality
+  -> scope:Locality.locality
   -> kind:Decls.logical_kind
   -> ?hook:Hook.t
   -> impargs:Impargs.manual_implicits
@@ -390,7 +384,7 @@ val declare_definition
 
 val declare_assumption
   :  name:Id.t
-  -> scope:locality
+  -> scope:Locality.locality
   -> hook:Hook.t option
   -> impargs:Impargs.manual_implicits
   -> uctx:UState.t
@@ -532,7 +526,7 @@ end
 
 val save_lemma_proved
   : proof:Proof.t
-  -> opaque:opacity_flag
+  -> opaque:Vernacexpr.opacity_flag
   -> idopt:Names.lident option
   -> unit
 
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 80a4de472c..ebec720ce2 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -64,12 +64,12 @@ GRAMMAR EXTEND Gram
       | IDENT "Existential"; n = natural; c = constr_body ->
           { VernacSolveExistential (n,c) }
       | IDENT "Admitted" -> { VernacEndProof Admitted }
-      | IDENT "Qed" -> { VernacEndProof (Proved (Declare.Opaque,None)) }
+      | IDENT "Qed" -> { VernacEndProof (Proved (Opaque,None)) }
       | IDENT "Save"; id = identref ->
-          { VernacEndProof (Proved (Declare.Opaque, Some id)) }
-      | IDENT "Defined" -> { VernacEndProof (Proved (Declare.Transparent,None)) }
+          { VernacEndProof (Proved (Opaque, Some id)) }
+      | IDENT "Defined" -> { VernacEndProof (Proved (Transparent,None)) }
       |	IDENT "Defined"; id=identref ->
-          { VernacEndProof (Proved (Declare.Transparent,Some id)) }
+          { VernacEndProof (Proved (Transparent,Some id)) }
       | IDENT "Restart" -> { VernacRestart }
       | IDENT "Undo" -> { VernacUndo 1 }
       | IDENT "Undo"; n = natural -> { VernacUndo n }
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 9209b95e34..c0105224bf 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -135,7 +135,7 @@ let rec solve_obligation prg num tac =
     then Error.depends user_num remaining
   in
   let obl = subst_deps_obl obls obl in
-  let scope = Declare.(Global Declare.ImportNeedQualified) 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_env evd (Global.env ()) in
@@ -303,7 +303,7 @@ let msg_generating_obl name obls =
 
 let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
     ?(impargs = []) ~poly
-    ?(scope = Declare.Global Declare.ImportDefaultBehavior)
+    ?(scope = Locality.Global Locality.ImportDefaultBehavior)
     ?(kind = Decls.(IsDefinition Definition)) ?tactic ?(reduce = reduce) ?hook
     ?(opaque = false) obls =
   let prg =
@@ -326,7 +326,7 @@ let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl)
     | _ -> res
 
 let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl)
-    ?tactic ~poly ?(scope = Declare.Global Declare.ImportDefaultBehavior)
+    ?tactic ~poly ?(scope = Locality.Global Locality.ImportDefaultBehavior)
     ?(kind = Decls.(IsDefinition Definition)) ?(reduce = reduce) ?hook ?(opaque = false)
     notations fixkind =
   let deps = List.map (fun ({Declare.Recthm.name; _}, _, _) -> name) l in
@@ -367,7 +367,7 @@ let admit_prog prg =
             let x = subst_deps_obl obls x in
             let uctx = Internal.get_uctx prg in
             let univs = UState.univ_entry ~poly:false uctx in
-            let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified
+            let kn = Declare.declare_constant ~name:x.obl_name ~local:Locality.ImportNeedQualified
               (Declare.ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural)
             in
               Declare.assumption_message x.obl_name;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 334f6d40bb..a3e0d3b5c1 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -73,7 +73,7 @@ val add_definition :
   -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
   -> ?impargs:Impargs.manual_implicits
   -> poly:bool
-  -> ?scope:Declare.locality
+  -> ?scope:Locality.locality
   -> ?kind:Decls.logical_kind
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(constr -> constr)
@@ -92,7 +92,7 @@ val add_mutual_definitions :
   -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
   -> ?tactic:unit Proofview.tactic
   -> poly:bool
-  -> ?scope:Declare.locality
+  -> ?scope:Locality.locality
   -> ?kind:Decls.logical_kind
   -> ?reduce:(constr -> constr)
   -> ?hook:Declare.Hook.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f7da2000e3..6295587844 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -466,7 +466,7 @@ let vernac_custom_entry ~module_local s =
 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) || Termops.is_section_variable id ||
-     locality <> Declare.Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
+     locality <> Locality.Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
   then
     user_err ?loc  (Id.print id ++ str " already exists.")
 
@@ -548,7 +548,6 @@ 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 Declare in
     match local with
     | Discharge -> Dumpglob.dump_definition lid true "var"
     | Global _ -> Dumpglob.dump_definition lid false "def"
@@ -604,7 +603,7 @@ let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
   let lemma, status = Declare.by (Tactics.exact_proof c) lemma in
-  let () = Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Opaque ~idopt:None in
+  let () = Declare.save_lemma_proved ~proof:lemma ~opaque:Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -614,8 +613,8 @@ let vernac_assumption ~atts discharge kind l nl =
     if Dumpglob.dump () then
       List.iter (fun (lid, _) ->
           match scope with
-            | Declare.Global _ -> Dumpglob.dump_definition lid false "ax"
-            | Declare.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
+            | Global _ -> Dumpglob.dump_definition lid false "ax"
+            | Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
   ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
 
 let is_polymorphic_inductive_cumulativity =
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 07c27dd849..62afdb92ff 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -74,7 +74,7 @@ module Declare : sig
     feedback_id:Stateid.t ->
     Declare.closed_proof_output Future.computation -> closed_proof
 
-  val close_proof : opaque:Declare.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
+  val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
 
   val discard_all : unit -> unit
   val update_global_env : unit -> unit