Merge PR #12499: Clean future goals

Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: ppedrot

1 files changed, 34 insertions, 35 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index d338b06e0e..db5265ca0a 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -167,6 +167,10 @@ val has_undefined : evar_map -> bool
 (** [has_undefined sigma] is [true] if and only if
     there are uninstantiated evars in [sigma]. *)
 
+val has_given_up : evar_map -> bool
+(** [has_given_up sigma] is [true] if and only if
+    there are given up evars in [sigma]. *)
+
 val new_evar : evar_map ->
   ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
 (** Creates a fresh evar mapping to the given information. *)
@@ -343,59 +347,54 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-type goal_kind = ToShelve | ToGiveUp
-
-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. *)
 
-val future_goals : evar_map -> Evar.t list
-(** Retrieves the list of future goals. Used by the [refine] primitive
-    of the tactic engine. *)
+module FutureGoals : sig
 
-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 t = private {
+    comb : Evar.t list;
+    shelf : Evar.t list;
+    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]. *)
+  }
 
-type future_goals
+  val map_filter : (Evar.t -> Evar.t option) -> t -> t
+  (** Applies a function on the 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. *)
+  val filter : (Evar.t -> bool) -> t -> t
+  (** Applies a filter on the future goals *)
 
-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. *)
+end
 
-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 push_future_goals : evar_map -> evar_map
 
-val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map
-(** Fold future goals *)
+val pop_future_goals : evar_map -> FutureGoals.t * evar_map
 
-val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals
-(** Applies a function on the future goals *)
+val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
 
-val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals
-(** Applies a filter on the future goals *)
+(** Fold future goals *)
+
+val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map
+(** Push goals on the shelve of future goals *)
 
-val dispatch_future_goals : future_goals -> Evar.t list * Evar.t list * Evar.t list * Evar.t option
-(** Returns the future_goals dispatched into regular, shelved, given_up
-   goals; last argument is the goal tagged as principal if any *)
+val remove_future_goal : evar_map -> Evar.t -> evar_map
 
-val extract_given_up_future_goals : future_goals -> Evar.t list * Evar.t list
-(** An ad hoc variant for Proof.proof; not for general use *)
+val give_up : Evar.t -> evar_map -> evar_map
 
-val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
-(** Push goals on the shelve of future goals *)
+val given_up : evar_map -> Evar.Set.t
 
 (** {5 Sort variables}