From 4e59a68fd6f2cd3cdf936c10cdbfeb46fc22ca95 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 11 Jun 2020 13:11:21 +0200
Subject: Better encapsulation of future goals

We try to encapsulate the future goals abstraction in the evar map.
A few calls to `save_future_goals` and `restore_future_goals` are still
there, but we try to minimize them.

This is a preliminary refactoring to make the invariants between the
shelf and future goals more explicit, before giving unification access
to the shelf, which is needed for #7825.
---
 engine/evd.mli | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index d338b06e0e..91cbbe5d77 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -378,23 +378,23 @@ val restore_future_goals : evar_map -> future_goals -> evar_map
     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
+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) -> future_goals -> future_goals
+val map_filter_future_goals : (Evar.t -> Evar.t option) -> evar_map -> evar_map
 (** Applies a function on the future goals *)
 
-val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals
+val filter_future_goals : (Evar.t -> bool) -> evar_map -> evar_map
 (** 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
+val dispatch_future_goals : evar_map -> 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
+val extract_given_up_future_goals : evar_map -> 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
+val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map
 (** Push goals on the shelve of future goals *)
 
 (** {5 Sort variables}
-- 
cgit v1.2.3