Put evars remaining after a tactic on the shelf.

Uses the new architecture which allows to keep track of all new evars. The [future_goals] are flushed at the end of the tactics, the [principal_future_goal] is ignored.

4 files changed, 22 insertions, 5 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index ee3c46f5c2..ef71dd04c8 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -57,6 +57,12 @@ module V82 = struct
 
   (* Old style mk_goal primitive *)
   let mk_goal evars hyps concl extra =
+    (* A goal created that way will not be used by refine and will not
+       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 prev_future_goals = Evd.future_goals evars in
+    let prev_principal_goal = Evd.principal_future_goal evars in
     let evi = { Evd.evar_hyps = hyps;
 		Evd.evar_concl = concl;
 		Evd.evar_filter = Evd.Filter.identity;
@@ -67,6 +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 ctxt = Environ.named_context_of_val hyps in
     let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in
     let ev = Term.mkEvar (evk,inst) in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8ad7adc166..53b73097f9 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -320,14 +320,15 @@ let run_tactic env tac pr =
   let sp = pr.proofview in
   let (_,tacticced_proofview,(status,(to_shelve,give_up))) = Proofview.apply env tac sp in
   let shelf =
-    let pre_shelf = pr.shelf@to_shelve in
-    (* avoid already to count already solved goals as shelved. *)
     Proofview.in_proofview tacticced_proofview begin fun sigma ->
+      let pre_shelf = pr.shelf@(Evd.future_goals sigma)@to_shelve in
+      (* avoid already to count already solved goals as shelved. *)
       List.filter (fun g -> Evd.is_undefined sigma g) pre_shelf
     end
   in
   let given_up = pr.given_up@give_up in
-  { pr with proofview = tacticced_proofview ; shelf ; given_up },status
+  let proofview = Proofview.reset_future_goals tacticced_proofview in
+  { pr with proofview ; shelf ; given_up },status
 
 let emit_side_effects eff pr =
   {pr with proofview = Proofview.emit_side_effects eff pr.proofview}
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 50076ed9f3..ea588d8e86 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -49,7 +49,10 @@ let init sigma =
   fun l ->
     let entry, v = aux l in
     (* Marks all the goal unresolvable for typeclasses. *)
-    entry, { v with solution = Typeclasses.mark_unresolvables v.solution }
+    let solution = Typeclasses.mark_unresolvables v.solution in
+    (* The created goal are not to be shelved. *)
+    let solution = Evd.reset_future_goals solution in
+    entry, { v with solution }
 
 type telescope =
   | TNil of Evd.evar_map
@@ -68,7 +71,10 @@ let dependent_init =
   fun t ->
     let entry, v = aux t in
     (* Marks all the goal unresolvable for typeclasses. *)
-    entry, { v with solution = Typeclasses.mark_unresolvables v.solution }
+    let solution = Typeclasses.mark_unresolvables v.solution in
+    (* The created goal are not to be shelved. *)
+    let solution = Evd.reset_future_goals solution in
+    entry, { v with solution }
 
 let initial_goals initial = initial
 
@@ -795,6 +801,8 @@ let numgoals =
 let in_proofview p k =
   k p.solution
 
+let reset_future_goals p =
+  { p with solution = Evd.reset_future_goals p.solution }
 
 
 module Notations = struct
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6d68cf4d46..d822f933be 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -313,6 +313,7 @@ module Monad : Monad.S with type +'a t = 'a tactic
 (*** Commands ***)
 
 val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
+val reset_future_goals : proofview -> proofview
 
 (* Notations for building tactics. *)
 module Notations : sig