From 4db82417bdda1f9b0c7ea6ba9f6d71c03cc07eba Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 23 Jan 2017 22:48:38 +0100
Subject: [stm] Remove unused legacy stm interface.

---
 stm/stm.ml  | 3 ---
 stm/stm.mli | 1 -
 2 files changed, 4 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 1cd6209aa4..fd1cefa8d1 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2954,9 +2954,6 @@ let proofname b = match VCS.get_branch b with
 let get_all_proof_names () =
   List.map unmangle (List.map_filter proofname (VCS.branches ()))
 
-let get_current_proof_name () =
-  Option.map unmangle (proofname (VCS.current_branch ()))
-
 (* Export hooks *)
 let state_computed_hook = Hooks.state_computed_hook
 let state_ready_hook = Hooks.state_ready_hook
diff --git a/stm/stm.mli b/stm/stm.mli
index 5d0d05d411..0f0a3c4e13 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -212,7 +212,6 @@ val interp : bool -> vernac_expr located -> unit
 (* Queries for backward compatibility *)
 val current_proof_depth : unit -> int
 val get_all_proof_names : unit -> Id.t list
-val get_current_proof_name : unit -> Id.t option
 
 (* Hooks to be set by other Coq components in order to break file cycles *)
 val process_error_hook : Future.fix_exn Hook.t
-- 
cgit v1.2.3