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.

1 files changed, 9 insertions, 2 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index cec6f0fad7..50076ed9f3 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