From 8cada511701d8893bab5553470ab721b33713043 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 19 Nov 2017 02:55:51 +0100
Subject: [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.
---
 ide/ide_slave.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 7cbab56d44..cfc0e09a0c 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 :: _ ->
-- 
cgit v1.2.3