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 /ide | |
| 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 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 7cbab56d4..cfc0e09a0 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -217,7 +217,7 @@ let evars () = let doc = get_doc () in set_doc @@ Stm.finish ~doc; let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let all_goals, _, _, _, sigma = Proof.proof pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in @@ -227,7 +227,7 @@ let evars () = let hints () = try let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let all_goals, _, _, _, sigma = Proof.proof pfts in match all_goals with | [] -> None | g :: _ -> |