Refine: proper scoping of the future goals.

In my first attempt I just dropped all future goals before starting a refinement. This was done for simplicity but is incorrect in general. In this version the future goals which are not introduced by the particular instance of refine are kept for future use.

3 files changed, 18 insertions, 2 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 35ca18e4f..b8886b9b5 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1007,6 +1007,9 @@ 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 =
+  { evd with future_goals = gls ; principal_future_goal = pgl }
+
 let meta_diff ext orig = 
   Metamap.fold (fun m v acc ->
     if Metamap.mem m orig then acc
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index c15975b0e..cc64b3594 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -301,6 +301,12 @@ 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
+(** 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
+    tactic engine. *)
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index cec6f0fad..50076ed9f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1028,10 +1028,15 @@ struct
     !evdref
 
   let refine ?(unsafe = false) f = Goal.enter begin fun gl ->
-    let sigma = Evd.reset_future_goals (Goal.sigma gl) in
+    let sigma = Goal.sigma gl in
     let env = Goal.env gl in
     let concl = Goal.concl gl in
-    let (sigma, c) = f sigma 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
+    (** Create the refinement term *)
+    let (sigma, c) = f (Evd.reset_future_goals sigma) in
     let evs = Evd.future_goals sigma in
     let evkmain = Evd.principal_future_goal sigma in
     (** Check that the introduced evars are well-typed *)
@@ -1046,6 +1051,8 @@ struct
           let id = Evd.evar_ident gl.Goal.self sigma in
           Evd.rename evk id (Evd.define gl.Goal.self c sigma)
     in
+    (** Restore the [future goals] state. *)
+    let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
     (** Select the goals *)
     let comb = undefined sigma (List.rev evs) in
     let sigma = List.fold_left mark_as_goal sigma comb in