diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 31132824f5..597e60093b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -967,9 +967,7 @@ module Search = struct let evm' = Evd.set_typeclass_evars evm' nongoals' in Some evm' in - let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply ~name ~poly env tac pv in - if not (List.is_empty gaveup) then - CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); + let (), pv', (unsafe, shelved), _ = Proofview.apply ~name ~poly env tac pv in if Proofview.finished pv' then finish pv' shelved else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found |