Make future_goals stack explicit in the evarmap

1 files changed, 20 insertions, 19 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index 4e3f95fc42..7a139e44ba 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -347,13 +347,11 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-type goal_kind = ToShelve
-
-val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
+val declare_future_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
     internal uses only. *)
 
-val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
+val declare_principal_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals and make
     it principal. Only one existential variable can be made principal, an
     error is raised otherwise. For internal uses only. *)
@@ -366,29 +364,30 @@ val principal_future_goal : evar_map -> Evar.t option
 (** Retrieves the name of the principal existential variable if there
     is one. Used by the [refine] primitive of the tactic engine. *)
 
-type future_goals
-
-val save_future_goals : evar_map -> future_goals
-(** Retrieves the list of future goals including the principal future
-    goal. Used by the [refine] primitive of the tactic engine. *)
+type future_goals = {
+  future_comb : Evar.t list;
+  future_shelf : Evar.t list;
+  future_principal : Evar.t option; (** if [Some e], [e] must be
+                                        contained in
+                                        [future_comb]. The evar
+                                        [e] will inherit
+                                        properties (now: the
+                                        name) of the evar which
+                                        will be instantiated with
+                                        a term containing [e]. *)
+}
 
-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 push_future_goals : evar_map -> evar_map
 
-val restore_future_goals : evar_map -> future_goals -> 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. *)
+val pop_future_goals : evar_map -> future_goals * evar_map
 
 val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
 (** Fold future goals *)
 
-val map_filter_future_goals : (Evar.t -> Evar.t option) -> evar_map -> evar_map
+val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals
 (** Applies a function on the future goals *)
 
-val filter_future_goals : (Evar.t -> bool) -> evar_map -> evar_map
+val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals
 (** Applies a filter on the future goals *)
 
 val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t option
@@ -398,6 +397,8 @@ val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t optio
 val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map
 (** Push goals on the shelve of future goals *)
 
+val remove_future_goal : evar_map -> Evar.t -> evar_map
+
 val give_up : Evar.t -> evar_map -> evar_map
 
 val given_up : evar_map -> Evar.Set.t