[declare] [api] Removal of deprecated functions

The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.

All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.

11 files changed, 4 insertions, 81 deletions

diff --git a/dev/base_include b/dev/base_include
index efbd156758..67ea3a1fa1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -111,10 +111,8 @@ open Search
 open Evar_refiner
 open Goal
 open Logic
-open Pfedit
 open Proof
 open Proof_using
-open Proof_global
 open Redexpr
 open Refiner
 open Tacmach
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 44c30598aa..9c82eb8960 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -174,7 +174,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
-  (* XXX: Using `DeclareDef.prepare_parameter` here directly is not
+  (* XXX: Using `Declare.prepare_parameter` here directly is not
      possible as we indeed declare several parameters; however,
      restrict_universe_context should be called in a centralized place
      IMO, thus I think we should adapt `prepare_parameter` to handle
@@ -202,7 +202,7 @@ let context_insection sigma ~poly ctx =
           else Monomorphic_entry Univ.ContextSet.empty
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
-        (* XXX Fixme: Use DeclareDef.prepare_definition *)
+        (* XXX Fixme: Use Declare.prepare_definition *)
         let uctx = Evd.evar_universe_context sigma in
         let kind = Decls.(IsDefinition Definition) in
         let _ : GlobRef.t =
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index e490b33dde..673124296d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -657,5 +657,3 @@ let make_cases ind =
        let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
        (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
     mip.mind_nf_lc []
-
-let declare_mutual_inductive_with_eliminations = DeclareInd.declare_mutual_inductive_with_eliminations
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 984581152a..9c876787a3 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -41,14 +41,6 @@ val do_mutual_inductive
 
 val make_cases : Names.inductive -> string list list
 
-val declare_mutual_inductive_with_eliminations
-  : ?primitive_expected:bool
-  -> Entries.mutual_inductive_entry
-  -> UnivNames.universe_binders
-  -> DeclareInd.one_inductive_impls list
-  -> Names.MutInd.t
-  [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
-
 val interp_mutual_inductive_constr
   : sigma:Evd.evar_map
   -> template:bool option
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c1f7eb53b3..fde332cb66 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1033,8 +1033,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
 
-let declare_universe_context = DeclareUctx.declare_universe_context
-
 type locality = Locality.locality = | Discharge | Global of import_status
 
 module CInfo = struct
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 6f104e764d..002328b63f 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -280,7 +280,7 @@ val fixpoint_message : int array option -> Id.t list -> unit
 
 val check_exists : Id.t -> unit
 
-(** {6 For legacy support, do not use}  *)
+(** {6 For internal support, do not use}  *)
 
 module Internal : sig
 
@@ -337,21 +337,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
 
-(** XXX: Temporarily re-exported for 3rd party code; don't use  *)
-val build_constant_by_tactic :
-  name:Names.Id.t ->
-  ?opaque:opacity_flag ->
-  uctx:UState.t ->
-  sign:Environ.named_context_val ->
-  poly:bool ->
-  EConstr.types ->
-  unit Proofview.tactic ->
-  Evd.side_effects proof_entry * bool * UState.t
-[@@ocaml.deprecated "This function is deprecated, used newer API in declare"]
-
-val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
-[@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"]
-
 type locality = Locality.locality = Discharge | Global of import_status
 
 (** Information for a constant *)
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
deleted file mode 100644
index 83bb1dae71..0000000000
--- a/vernac/declareDef.ml
+++ /dev/null
@@ -1,9 +0,0 @@
-type locality = Declare.locality =
-  | Discharge [@ocaml.deprecated "Use [Declare.Discharge]"]
-  | Global of Declare.import_status [@ocaml.deprecated "Use [Declare.Global]"]
-[@@ocaml.deprecated "Use [Declare.locality]"]
-
-let declare_definition = Declare.declare_definition
-[@@ocaml.deprecated "Use [Declare.declare_definition]"]
-module Hook = Declare.Hook
-[@@ocaml.deprecated "Use [Declare.Hook]"]
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 76e2f5cb2c..334f6d40bb 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -52,14 +52,10 @@ open Constr
 {2} Saving of obligations: as open obligations use the regular proof
    mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason
    obligations code is split in two: this file, [Obligations], taking
-   care of the top-level vernac commands, and [DeclareObl], which is
+   care of the top-level vernac commands, and [Declare], which is
    called by `Lemmas` to close an obligation proof and eventually to
    declare the top-level [Program]ed constant.
 
-    There is little obligations-specific code in [DeclareObl], so
-   eventually that file should be integrated in the regular [Declare]
-   path, as it gains better support for "dependent_proofs".
-
  *)
 
 val default_tactic : unit Proofview.tactic ref
diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml
deleted file mode 100644
index 150311ffaa..0000000000
--- a/vernac/pfedit.ml
+++ /dev/null
@@ -1,19 +0,0 @@
-(* Compat API / *)
-let get_current_context = Declare.get_current_context
-[@@ocaml.deprecated "Use [Declare.get_current_context]"]
-let solve = Proof.solve
-[@@ocaml.deprecated "Use [Proof.solve]"]
-let by = Declare.by
-[@@ocaml.deprecated "Use [Declare.by]"]
-let refine_by_tactic = Proof.refine_by_tactic
-[@@ocaml.deprecated "Use [Proof.refine_by_tactic]"]
-
-(* We don't want to export this anymore, but we do for now *)
-let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac =
-  let b, t, _unis, safe, uctx =
-    Declare.build_by_tactic ?side_eff env ~uctx ~poly ~typ tac in
-  b, t, safe, uctx
-[@@ocaml.deprecated "Use [Proof.build_by_tactic]"]
-
-let build_constant_by_tactic = Declare.build_constant_by_tactic [@ocaml.warning "-3"]
-[@@ocaml.deprecated "Use [Proof.build_constant_by_tactic]"]
diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml
deleted file mode 100644
index 2c66b3e26c..0000000000
--- a/vernac/proof_global.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-(* compatibility module; can be removed once we agree on the API *)
-
-type t = Declare.Proof.t
-[@@ocaml.deprecated "Use [Declare.Proof.t]"]
-let map_proof = Declare.Proof.map
-[@@ocaml.deprecated "Use [Declare.Proof.map_proof]"]
-let get_proof = Declare.Proof.get
-[@@ocaml.deprecated "Use [Declare.Proof.get_proof]"]
-
-type opacity_flag = Declare.opacity_flag =
-  | Opaque [@ocaml.deprecated "Use [Declare.Opaque]"]
-  | Transparent [@ocaml.deprecated "Use [Declare.Transparent]"]
-[@@ocaml.deprecated "Use [Declare.opacity_flag]"]
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index c30703d734..78f9b6098a 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -44,6 +44,3 @@ ComArguments
 Vernacentries
 Vernacstate
 Vernacinterp
-Proof_global
-Pfedit
-DeclareDef