From bfb393596b1df815a109c9c600b9a2b413561fcb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 09:30:26 +0100
Subject: Proof engine: using save_future_goal when relevant.

---
 engine/proofview.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 4f8da53787..73f26c3208 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -769,9 +769,8 @@ let with_shelf tac =
   Pv.get >>= fun npv ->
   let { shelf = gls; solution = sigma } = npv in
   let gls' = Evd.future_goals sigma in
-  let fgoals = Evd.future_goals solution in
-  let pgoal = Evd.principal_future_goal solution in
-  let sigma = Evd.restore_future_goals sigma (fgoals,pgoal) in
+  let fgoals = Evd.save_future_goals solution in
+  let sigma = Evd.restore_future_goals sigma fgoals in
   (* Ensure we mark and return only unsolved goals *)
   let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
   let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
-- 
cgit v1.2.3