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 /printing/printer.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 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 3c31dd96b..d6f0778f7 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -17,7 +17,6 @@ open Nametab open Evd open Proof_type open Refiner -open Pfedit open Constrextern open Ppconstr open Declarations @@ -812,7 +811,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = end let pr_nth_open_subgoal n = - let pf = get_pftreestate () in + let pf = Proof_global.give_me_the_proof () in let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in pr_subgoal n sigma gls |