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, 6 insertions, 0 deletions

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