Make future_goals stack explicit in the evarmap

3 files changed, 22 insertions, 29 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7aea07d6f0..e8f2ab5674 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -56,18 +56,12 @@ module V82 = struct
        be shelved. It must not appear as a future_goal, so the future
        goals are restored to their initial value after the evar is
        created. *)
+    let evars = Evd.push_future_goals evars in
     let inst = EConstr.identity_subst_val hyps in
-    let evi = { Evd.evar_hyps = hyps;
-                Evd.evar_concl = concl;
-                Evd.evar_filter = Evd.Filter.identity;
-                Evd.evar_abstract_arguments = Evd.Abstraction.identity;
-                Evd.evar_body = Evd.Evar_empty;
-                Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
-                Evd.evar_candidates = None;
-                Evd.evar_identity = Evd.Identity.make inst;
-              }
+    let (evars,evk) =
+      Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl
     in
-    let (evars, evk) = Evd.new_evar evars ~typeclass_candidate:false evi in
+    let _, evars = Evd.pop_future_goals evars in
     let ev = EConstr.mkEvar (evk,inst) in
     (evk, ev, evars)
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 23998f8ba1..11a8023ab6 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -363,28 +363,28 @@ let update_sigma_env p env =
 
 let run_tactic env tac pr =
   let open Proofview.Notations in
-  let sp = pr.proofview in
   let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in
   let tac =
     tac >>= fun result ->
     Proofview.tclEVARMAP >>= fun sigma ->
     (* Already solved goals are not to be counted as shelved. Nor are
       they to be marked as unresolvable. *)
-    let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) sigma in
-    let retrieved = List.rev @@ Evd.future_goals retrieved in
+    let retrieved, sigma = Evd.pop_future_goals sigma in
+    let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) retrieved in
+    let retrieved = List.rev_append retrieved.Evd.future_shelf (List.rev retrieved.Evd.future_comb) in
     let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT (result,retrieved)
   in
-  let { name; poly } = pr in
+  let { name; poly; proofview } = pr in
+  let proofview = Proofview.Unsafe.push_future_goals proofview in
   let ((result,retrieved),proofview,(status,to_shelve),info_trace) =
-    Proofview.apply ~name ~poly env tac sp
+    Proofview.apply ~name ~poly env tac proofview
   in
   let sigma = Proofview.return proofview in
   let to_shelve = undef sigma to_shelve in
   let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in
   let proofview = Proofview.Unsafe.mark_as_unresolvables proofview to_shelve in
-  let proofview = Proofview.Unsafe.reset_future_goals proofview in
   { pr with proofview ; shelf },(status,info_trace),result
 
 (*** Commands ***)
@@ -569,7 +569,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
   let eff = Evd.eval_side_effects sigma in
   let sigma = Evd.drop_side_effects sigma in
   (* Save the existing goals *)
-  let prev_future_goals = Evd.save_future_goals sigma in
+  let sigma = Evd.push_future_goals sigma in
   (* Start a proof *)
   let prf = start ~name ~poly sigma [env, ty] in
   let (prf, _, ()) =
@@ -593,12 +593,12 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
   let sigma = Evd.drop_side_effects sigma in
   let sigma = Evd.emit_side_effects eff sigma in
   (* Restore former goals *)
-  let sigma = Evd.restore_future_goals sigma prev_future_goals in
+  let _goals, sigma = Evd.pop_future_goals sigma in
   (* Push remaining goals as future_goals which is the only way we
      have to inform the caller that there are goals to collect while
      not being encapsulated in the monad *)
   (* Goals produced by tactic "shelve" *)
-  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
+  let sigma = List.fold_right (Evd.declare_future_goal ~shelve:true) shelf sigma in
   (* Other goals *)
   let sigma = List.fold_right Evd.declare_future_goal goals sigma in
   (* Get rid of the fresh side-effects by internalizing them in the term
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 4244a9c900..7f0fa587cd 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -51,9 +51,9 @@ 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.save_future_goals sigma in
+  let sigma = Evd.push_future_goals sigma in
   (* Create the refinement term *)
-  Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
+  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
   f >>= fun (v, c) ->
   Proofview.tclEVARMAP >>= fun sigma' ->
   Proofview.V82.wrap_exceptions begin fun () ->
@@ -72,17 +72,16 @@ let generic_refine ~typecheck f gl =
     else Pretype_errors.error_occur_check env sigma self c
   in
   (* Restore the [future goals] state. *)
-  let sigma = Evd.restore_future_goals sigma prev_future_goals in
+  let future_goals, sigma = Evd.pop_future_goals sigma in
   (* Select the goals *)
-  let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) sigma' in
-  let comb,shelf,evkmain = Evd.dispatch_future_goals evs in
+  let future_goals = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) future_goals in
   (* Proceed to the refinement *)
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->
     (* Nothing to do, the goal has been solved by side-effect *)
     sigma
   | Some self ->
-    match evkmain with
+    match future_goals.Evd.future_principal with
     | None -> Evd.define self c sigma
     | Some evk ->
         let id = Evd.evar_ident self sigma in
@@ -92,16 +91,16 @@ let generic_refine ~typecheck f gl =
         | Some id -> Evd.rename evk id sigma
   in
   (* Mark goals *)
-  let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
-  let sigma = Proofview.Unsafe.mark_unresolvables sigma shelf in
-  let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
+  let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.future_comb in
+  let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.future_shelf in
+  let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.future_comb in
   let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
                                    Termops.Internal.print_constr_env env sigma c)) in
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
-  Proofview.Unsafe.tclPUTSHELF shelf <*>
+  Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.future_shelf <*>
   Proofview.tclUNIT v
   end