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

---
 engine/proofview.ml | 5 ++---
 proofs/goal.ml      | 5 ++---
 proofs/refine.ml    | 5 ++---
 3 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 4f8da5378..73f26c320 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
diff --git a/proofs/goal.ml b/proofs/goal.ml
index e153aa277..ba7e458f3 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -62,8 +62,7 @@ module V82 = struct
        goals are restored to their initial value after the evar is
        created. *)
     let concl = EConstr.Unsafe.to_constr concl in
-    let prev_future_goals = Evd.future_goals evars in
-    let prev_principal_goal = Evd.principal_future_goal evars in
+    let prev_future_goals = Evd.save_future_goals evars in
     let evi = { Evd.evar_hyps = hyps;
 		Evd.evar_concl = concl;
 		Evd.evar_filter = Evd.Filter.identity;
@@ -74,7 +73,7 @@ module V82 = struct
     in
     let evi = Typeclasses.mark_unresolvable evi in
     let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
-    let evars = Evd.restore_future_goals evars (prev_future_goals,prev_principal_goal) in
+    let evars = Evd.restore_future_goals evars prev_future_goals in
     let ctxt = Environ.named_context_of_val hyps in
     let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
     let ev = EConstr.mkEvar (evk,inst) in
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 39d77d983..b5578a187 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -78,8 +78,7 @@ let generic_refine ~typecheck f gl =
   let state = Proofview.Goal.state gl in
   (** Save the [future_goals] state to restore them after the
       refinement. *)
-  let prev_future_goals = Evd.future_goals sigma in
-  let prev_principal_goal = Evd.principal_future_goal sigma in
+  let prev_future_goals = Evd.save_future_goals sigma in
   (** Create the refinement term *)
   Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
   f >>= fun (v, c) ->
@@ -119,7 +118,7 @@ let generic_refine ~typecheck f gl =
         | Some id -> Evd.rename evk id sigma
   in
   (** Restore the [future goals] state. *)
-  let sigma = Evd.restore_future_goals sigma (prev_future_goals,prev_principal_goal) in
+  let sigma = Evd.restore_future_goals sigma prev_future_goals in
   (** Select the goals *)
   let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
-- 
cgit v1.2.3