diff options
| author | Maxime Dénès | 2020-06-11 13:11:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-26 16:38:34 +0200 |
| commit | 4e59a68fd6f2cd3cdf936c10cdbfeb46fc22ca95 (patch) | |
| tree | 0bdb09f0eae78a88b855ebcff4da3e2a9b363800 /tactics/class_tactics.ml | |
| parent | 4e6b029805a74ea16166da2c5f59f9669fd34eb8 (diff) | |
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.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |