From 9402b6efad32757f44d72d83f6aabdca8829e3ed Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 7 Nov 2017 00:48:14 +0100
Subject: [api] Remove 8.7 ML-deprecated functions.

---
 API/API.mli | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index ccb71179dd..074b79efcf 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
 
-- 
cgit v1.2.3