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.
---
 proofs/proof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/proof.ml')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 38fcdd6e5f..c427c07b93 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -373,7 +373,7 @@ let run_tactic env tac pr =
     Proofview.tclEVARMAP >>= fun sigma ->
     (* Already solved goals are not to be counted as shelved. Nor are
       they to be marked as unresolvable. *)
-    let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in
+    let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) sigma in
     let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in
     (* Check that retrieved given up is empty *)
     if not (List.is_empty retrieved_given_up) then
-- 
cgit v1.2.3