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 /engine/evarutil.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 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 01c4e5fd72..9d3ae95e7d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -522,9 +522,7 @@ let restrict_evar evd evk filter ?src candidates = let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in (* Mark new evar as future goal, removing previous one, circumventing Proofview.advance but making Proof.run_tactic catch these. *) - let future_goals = Evd.save_future_goals evd in - let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in - let evd = Evd.restore_future_goals evd future_goals in + let evd = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) evd in (Evd.declare_future_goal evk' evd, evk') let rec check_and_clear_in_constr env evdref err ids global c = |