From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Jun 2017 06:08:02 +0200
Subject: [proof] Deprecate redundant wrappers.

As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.

We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index a79bf54267..1580b451d0 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -931,7 +931,7 @@ let show_script ?proof () =
   try
     let prf =
       try match proof with
-      | None -> Some (Pfedit.get_current_proof_name ())
+      | None -> Some (Proof_global.get_current_proof_name ())
       | Some (p,_) -> Some (p.Proof_global.id)
       with Proof_global.NoCurrentProof -> None
     in
-- 
cgit v1.2.3