diff options
Diffstat (limited to 'tactics')
| -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 |