diff options
| author | Pierre-Marie Pédrot | 2020-08-27 16:23:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-27 16:23:44 +0200 |
| commit | 2062f9cd5ce3c17c128186d1e9e2193528941e5c (patch) | |
| tree | edd7cf41caeedae18d60dc5c859e2532884ab80a /engine/evarutil.ml | |
| parent | 829d7ac10175c41eaf3ce8ad9531abeab713dcba (diff) | |
| parent | bd00733ef04e4c916ab4a00d80e9ee1142bcd410 (diff) | |
Merge PR #12499: Clean future goals
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: ppedrot
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..7beb7ff738 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.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 = |