diff options
| author | Maxime Dénès | 2020-06-12 01:18:27 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-26 16:38:34 +0200 |
| commit | 6c2a5cba55a831e461e806e08c7be968f9343f7e (patch) | |
| tree | 1ce5dee2ba387ef806879abbbf0414a9389e4a9b /engine/evarutil.ml | |
| parent | 46c0b7ab3653a6f1ef4b40466c2dd130d09136cb (diff) | |
Make future_goals stack explicit in the evarmap
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 9d3ae95e7d..7beb7ff738 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -522,7 +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 evd = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) evd in + let evd = Evd.remove_future_goal evd evk in (Evd.declare_future_goal evk' evd, evk') let rec check_and_clear_in_constr env evdref err ids global c = |