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.
---
 tactics/class_tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 2f55cc071f..31132824f5 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -934,7 +934,6 @@ module Search = struct
        let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>=
          fun stuck -> Proofview.shelve_goals (List.map Proofview_monad.drop_state stuck) in
        let evm = Evd.set_typeclass_evars evm Evar.Set.empty in
-       let fgoals = Evd.save_future_goals evm in
        let _, pv = Proofview.init evm [] in
        let pv = Proofview.unshelve goalsl pv in
        try
@@ -956,7 +955,8 @@ module Search = struct
                          (str "leaking evar " ++ int (Evar.repr ev) ++
                             spc () ++ pr_ev evm' ev);
                      acc && okev) evm' true);
-           let fgoals = Evd.shelve_on_future_goals shelved fgoals in
+           let evm = Evd.shelve_on_future_goals shelved evm in
+           let fgoals = Evd.save_future_goals evm in
            let evm' = Evd.restore_future_goals evm' fgoals in
            let nongoals' =
              Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with
-- 
cgit v1.2.3