From 7d2a9df50d519607c23a97c8973cb7d026d3d8d0 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 7 Jul 2018 21:17:32 -0400
Subject: Code to handle "Back" command for diffs.

---
 ide/idetop.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 854b1abe31..417ade51fd 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -211,15 +211,13 @@ let add_diffs oldp newp intf =
     { intf with fg_goals = { first_goal with goal_hyp = hyps_pp_list; goal_ccl = concl_pp } :: tl }
 
 let goals () =
-  let oldp =
-    try Some (Proof_global.give_me_the_proof ())
-    with Proof_global.NoCurrentProof -> None in
   let doc = get_doc () in
   set_doc @@ Stm.finish ~doc;
   try
     let newp = Proof_global.give_me_the_proof () in
     let intf = export_pre_goals (Proof.map_structured_proof newp process_goal) in
     if Proof_diffs.show_diffs () then
+      let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
       try
         Some (add_diffs oldp (Some newp) intf)
       with Pp_diff.Diff_Failure _ -> Some intf
-- 
cgit v1.2.3