diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 6651ff5f63..d91b90caa2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -462,7 +462,12 @@ let new_evar evd ?naming evi = let remove d e = let undf_evars = EvMap.remove e d.undf_evars in let defn_evars = EvMap.remove e d.defn_evars in - { d with undf_evars; defn_evars; } + let principal_future_goal = match d.principal_future_goal with + | None -> None + | Some e' -> if Evar.equal e e' then None else d.principal_future_goal + in + let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in + { d with undf_evars; defn_evars; principal_future_goal; future_goals } let find d e = try EvMap.find e d.undf_evars |