diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 02:55:51 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 03:03:36 +0100 |
commit | 8cada511701d8893bab5553470ab721b33713043 (patch) | |
tree | cb9cc69cdb9c89b973c923f753e85b68a1ac27f3 /printing | |
parent | edf1a8f36f75861b822081b3825357e122b6937d (diff) |
[proof] Attempt to deprecate some V82 parts of the proof API.
I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.
However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.
Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.
Diffstat (limited to 'printing')
-rw-r--r-- | printing/printer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 075b03b7d..ba31b72d6 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -828,7 +828,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = let pr_nth_open_subgoal n = let pf = Proof_global.give_me_the_proof () in - let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in + let gls,_,_,_,sigma = Proof.proof pf in pr_subgoal n sigma gls let pr_goal_by_id id = |