[api] Remove 8.7 ML-deprecated functions.

12 files changed, 6 insertions, 172 deletions

diff --git a/API/API.mli b/API/API.mli
index ccb71179d..074b79efc 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2122,7 +2122,6 @@ sig
       elim  : Globnames.global_reference;
       intro : Globnames.global_reference;
       typ   : Globnames.global_reference }
-  val gen_reference : string -> string list -> string -> Globnames.global_reference
   val find_reference : string -> string list -> string -> Globnames.global_reference
   val check_required_library : string list -> unit
   val logic_module_name : string list
@@ -4730,14 +4729,6 @@ sig
     unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind))
 
   val get_current_context : unit -> Evd.evar_map * Environ.env
-
-  (* Deprecated *)
-  val delete_current_proof : unit -> unit
-  [@@ocaml.deprecated "use Proof_global.discard_current"]
-
-  val get_current_proof_name : unit -> Names.Id.t
-  [@@ocaml.deprecated "use Proof_global.get_current_proof_name"]
-
   val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types
 end
 
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 5be8257e8..707adce30 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -24,6 +24,12 @@ passing `-bypass-API`.
 
 ### ML API
 
+General deprecation
+
+- All functions marked [@@ocaml.deprecated] in 8.7 have been
+  removed. Please, make sure your plugin is warning-free in 8.7 before
+  trying to port it over 8.8.
+
 We removed the following functions:
 
 - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context`
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 3f4e8aa12..94357aad3 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -137,8 +137,3 @@ let handled e =
   let bottom _ = raise Bottom in
   try let _ = print_gen bottom !handle_stack e in true
   with Bottom -> false
-
-(* Deprecated functions *)
-let error            string = user_err (str string)
-let user_err_loc (loc,hdr,msg) = user_err ~loc ~hdr msg
-let errorlabstrm hdr msg = user_err ~hdr msg
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index f3253979f..6fcc97a91 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -93,14 +93,3 @@ val noncritical : exn -> bool
 (** Check whether an exception is handled by some toplevel printer. The
     [Anomaly] exception is never handled. *)
 val handled : exn -> bool
-
-(** Deprecated functions  *)
-val error : string -> 'a
- [@@ocaml.deprecated "use [user_err] instead"]
-
-val errorlabstrm : string -> Pp.t -> 'a
- [@@ocaml.deprecated "use [user_err ~hdr] instead"]
-
-val user_err_loc : Loc.t * string * Pp.t -> 'a
- [@@ocaml.deprecated "use [user_err ~loc] instead"]
-
diff --git a/lib/flags.ml b/lib/flags.ml
index a53a866ab..323b5492d 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -140,10 +140,6 @@ let verbosely f x = without_option quiet f x
 let if_silent f x = if !quiet then f x
 let if_verbose f x = if not !quiet then f x
 
-let make_silent flag = quiet := flag
-let is_silent () = !quiet
-let is_verbose () = not !quiet
-
 let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = !auto_intros
diff --git a/lib/flags.mli b/lib/flags.mli
index 5233e72a2..0ff3e0a81 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -87,14 +87,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
-(* Deprecated *)
-val make_silent : bool -> unit
-[@@ocaml.deprecated "Please use Flags.quiet"]
-val is_silent : unit -> bool
-[@@ocaml.deprecated "Please use Flags.quiet"]
-val is_verbose : unit -> bool
-[@@ocaml.deprecated "Please use Flags.quiet"]
-
 (* Miscellaneus flags for vernac *)
 val make_auto_intros : bool -> unit
 val is_auto_intros : unit -> bool
diff --git a/lib/loc.ml b/lib/loc.ml
index 4a935a9d9..2cf4d3960 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -84,9 +84,3 @@ let raise ?loc e =
     let info = Exninfo.add Exninfo.null location loc in
     Exninfo.iraise (e, info)
 
-(** Deprecated *)
-let located_fold_left f x (_,a) = f x a
-let located_iter2 f (_,a) (_,b) = f a b
-let down_located f (_,a) = f a
-
-
diff --git a/lib/loc.mli b/lib/loc.mli
index fde490cc8..800940f21 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -65,14 +65,3 @@ val tag : ?loc:t -> 'a -> 'a located
 
 val map : ('a -> 'b) -> 'a located -> 'b located
 (** Modify an object carrying a location *)
-
-(** Deprecated functions  *)
-val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
- [@@ocaml.deprecated "use pattern matching"]
-
-val down_located : ('a -> 'b) -> 'a located -> 'b
- [@@ocaml.deprecated "use pattern matching"]
-
-val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
- [@@ocaml.deprecated "use pattern matching"]
-
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 8787738af..141fff033 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -377,7 +377,3 @@ let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
 let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
 let coq_or_ref     = lazy (init_reference ["Logic"] "or")
 let coq_iff_ref    = lazy (init_reference ["Logic"] "iff")
-
-(* Deprecated *)
-let gen_reference = coq_reference
-
diff --git a/library/coqlib.mli b/library/coqlib.mli
index 1e3c37a9e..b560cabb6 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -205,7 +205,3 @@ val coq_sig_ref : global_reference lazy_t
 
 val coq_or_ref : global_reference lazy_t
 val coq_iff_ref : global_reference lazy_t
-
-(* Deprecated functions *)
-val gen_reference :  message -> string list -> string -> global_reference
-[@@ocaml.deprecated "Please use Coqlib.find_reference"]
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 469e1a011..2d4aba17c 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -230,31 +230,3 @@ let apply_implicit_tactic tac = (); fun env sigma evk ->
 let solve_by_implicit_tactic () = match !implicit_tactic with
 | None -> None
 | Some tac -> Some (apply_implicit_tactic tac)
-
-(** Deprecated functions  *)
-let refining = Proof_global.there_are_pending_proofs
-let check_no_pending_proofs = Proof_global.check_no_pending_proof
-
-let get_current_proof_name = Proof_global.get_current_proof_name
-let get_all_proof_names = Proof_global.get_all_proof_names
-
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-
-let delete_proof = Proof_global.discard
-let delete_current_proof = Proof_global.discard_current
-let delete_all_proofs = Proof_global.discard_all
-
-let get_pftreestate () =
-  Proof_global.give_me_the_proof ()
-
-let set_end_tac tac =
-  Proof_global.set_endline_tactic tac
-
-let set_used_variables l =
-  Proof_global.set_used_variables l
-
-let get_used_variables () =
-  Proof_global.get_used_variables ()
-
-let get_universe_decl () =
-  Proof_global.get_universe_decl ()
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6e4ecd13b..adfe33786 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -8,7 +8,6 @@
 
 (** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
 
-open Loc
 open Names
 open Term
 open Environ
@@ -122,84 +121,3 @@ val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
 val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
-
-(** {5 Deprecated functions in favor of [Proof_global]} *)
-
-(** {6 ... } *)
-(** Several proofs can be opened simultaneously but at most one is
-   focused at some time. The following functions work by side-effect
-   on current set of open proofs. In this module, ``proofs'' means an
-   open proof (something started by vernacular command [Goal], [Lemma]
-   or [Theorem]), and ``goal'' means a subgoal of the current focused
-   proof *)
-
-(** [refining ()] tells if there is some proof in progress, even if a not
-   focused one *)
-
-val refining : unit -> bool
-[@@ocaml.deprecated "use Proof_global.there_are_pending_proofs"]
-
-(** [check_no_pending_proofs ()] fails if there is still some proof in
-   progress *)
-
-val check_no_pending_proofs : unit -> unit
-[@@ocaml.deprecated "use Proof_global.check_no_pending_proofs"]
-
-(** {6 ... } *)
-(** [delete_proof name] deletes proof of name [name] or fails if no proof
-    has this name *)
-
-val delete_proof : Id.t located -> unit
-[@@ocaml.deprecated "use Proof_global.discard"]
-
-(** [delete_current_proof ()] deletes current focused proof or fails if
-    no proof is focused *)
-
-val delete_current_proof : unit -> unit
-[@@ocaml.deprecated "use Proof_global.discard_current"]
-
-(** [delete_all_proofs ()] deletes all open proofs if any *)
-val delete_all_proofs : unit -> unit
-[@@ocaml.deprecated "use Proof_global.discard_all"]
-
-(** [get_pftreestate ()] returns the current focused pending proof.
-   @raise NoCurrentProof if there is no pending proof. *)
-
-val get_pftreestate : unit -> Proof.proof
-[@@ocaml.deprecated "use Proof_global.give_me_the_proof"]
-
-(** {6 ... } *)
-(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
-    by [solve] *)
-
-val set_end_tac : Genarg.glob_generic_argument -> unit
-[@@ocaml.deprecated "use Proof_global.set_endline_tactic"]
-
-(** {6 ... } *)
-(** [set_used_variables l] declares that section variables [l] will be
-    used in the proof *)
-val set_used_variables :
-  Id.t list -> Context.Named.t * Names.Id.t Loc.located list
-[@@ocaml.deprecated "use Proof_global.set_used_variables"]
-
-val get_used_variables : unit -> Context.Named.t option
-[@@ocaml.deprecated "use Proof_global.get_used_variables"]
-
-(** {6 Universe binders } *)
-val get_universe_decl : unit -> Univdecls.universe_decl
-[@@ocaml.deprecated "use Proof_global.get_universe_decl"]
-
-(** {6 ... } *)
-(** [get_current_proof_name ()] return the name of the current focused
-    proof or failed if no proof is focused *)
-val get_current_proof_name : unit -> Id.t
-[@@ocaml.deprecated "use Proof_global.get_current_proof_name"]
-
-(** [get_all_proof_names ()] returns the list of all pending proof names.
-    The first name is the current proof, the other names may come in
-    any order. *)
-val get_all_proof_names : unit -> Id.t list
-[@@ocaml.deprecated "use Proof_global.get_all_proof_names"]
-
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-[@@ocaml.deprecated "use Proof_global.lemma_possible_guards"]