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

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

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

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)

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) =

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

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

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
 

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

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,22 +86,22 @@ 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 *)
       let typ = replace_vars subst typ in
       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

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

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

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

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  *)

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

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