Proof engine: consider the pair principal and future goals as an entity.

6 files changed, 6 insertions, 6 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 185cab101..e0453713e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -946,7 +946,7 @@ let principal_future_goal evd = evd.principal_future_goal
 let reset_future_goals evd =
   { evd with future_goals = [] ; principal_future_goal=None }
 
-let restore_future_goals evd gls pgl =
+let restore_future_goals evd (gls,pgl) =
   { evd with future_goals = gls ; principal_future_goal = pgl }
 
 (**********************************************************)
diff --git a/engine/evd.mli b/engine/evd.mli
index 49c953f6d..49632d2e7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -303,7 +303,7 @@ val reset_future_goals : evar_map -> evar_map
 (** Clears the list of future goals (as well as the principal future
     goal). Used by the [refine] primitive of the tactic engine. *)
 
-val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map
+val restore_future_goals : evar_map -> Evar.t list * Evar.t option -> evar_map
 (** Sets the future goals (including the principal future goal) to a
     previous value. Intended to be used after a local list of future
     goals has been consumed. Used by the [refine] primitive of the
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 8a844bbf5..4f8da5378 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -771,7 +771,7 @@ let with_shelf tac =
   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 sigma = Evd.restore_future_goals sigma (fgoals,pgoal) 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 ed0d76f93..e153aa277 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -74,7 +74,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,prev_principal_goal) 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 50fd1c472..39d77d983 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -119,7 +119,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,prev_principal_goal) 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
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9f6624889..f386e804e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -983,7 +983,7 @@ module Search = struct
                           (str "leaking evar " ++ int (Evar.repr ev) ++
                              spc () ++ pr_ev evm' ev);
                       acc && okev) evm' true);
-           let evm' = Evd.restore_future_goals evm' (shelved @ fgoals) pgoal in
+           let evm' = Evd.restore_future_goals evm' (shelved @ fgoals, pgoal) in
            let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
            Some evm'
          else raise Not_found