From d2c50bb29df8f0b23f7ee498abeda43a672fc688 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 08:58:50 +0100
Subject: Proof engine: consider the pair principal and future goals as an
 entity.

---
 engine/evd.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 49c953f6d3..49632d2e76 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -303,7 +303,7 @@ 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
+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
-- 
cgit v1.2.3


From e508aec3a90aca93c188c54b707d19114ef5ff83 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 09:01:45 +0100
Subject: Proof engine: adding a function to save future goals including
 principal one.

---
 engine/evd.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 49632d2e76..44ec4a7e5c 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -299,6 +299,10 @@ 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. *)
 
+val save_future_goals : evar_map -> Evar.t list * Evar.t option
+(** Retrieves the list of future goals including the principal future
+    goal. Used by the [refine] primitive of the tactic engine. *)
+
 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. *)
-- 
cgit v1.2.3


From 6f30f76def8f6cf1abe7859f482b68c91b4c8709 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 09:32:51 +0100
Subject: Proof engine: support for nesting tactic-in-term within other
 tactics.

Tactic-in-term can be called from within a tactic itself. We have to
preserve the preexisting future_goals (if called from pretyping) and
we have to inform of the existence of pending goals, using
future_goals which is the only way to tell it in the absence of being
part of an encapsulating proofview.

This fixes #6313.

Conversely, future goals, created by pretyping, can call ltac:(giveup) or
ltac:(shelve), and this has to be remembered. So, we do it.
---
 engine/evd.mli | 31 +++++++++++++++++++++++++++----
 1 file changed, 27 insertions(+), 4 deletions(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 44ec4a7e5c..bd9d75c6b0 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -282,11 +282,13 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-val declare_future_goal : Evar.t -> evar_map -> evar_map
+type goal_kind = ToShelve | ToGiveUp
+
+val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
     internal uses only. *)
 
-val declare_principal_goal : Evar.t -> evar_map -> evar_map
+val declare_principal_goal : ?tag:goal_kind -> 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. *)
@@ -299,7 +301,9 @@ 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. *)
 
-val save_future_goals : evar_map -> Evar.t list * Evar.t option
+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. *)
 
@@ -307,12 +311,31 @@ 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
+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 fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map
+(** Fold future goals *)
+
+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) -> future_goals -> future_goals
+(** Applies a filter on the 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 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 shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
+(** Push goals on the shelve of future goals *)
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
-- 
cgit v1.2.3