diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-11 06:08:02 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-11 15:54:48 +0200 |
commit | f610068823b33bdc0af752a646df05b98489d7ce (patch) | |
tree | 5d664bd1b3efb43536250b30b0dffa724e28dba4 /stm/stm.ml | |
parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) |
[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`.
Diffstat (limited to 'stm/stm.ml')
-rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index a79bf5426..1580b451d 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 |