diff options
| author | Maxime Dénès | 2020-06-11 18:51:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-26 16:38:34 +0200 |
| commit | 46c0b7ab3653a6f1ef4b40466c2dd130d09136cb (patch) | |
| tree | b6937b47990e5f76b3f9a5b0fc8999754334ce26 /tactics/class_tactics.ml | |
| parent | 4e59a68fd6f2cd3cdf936c10cdbfeb46fc22ca95 (diff) | |
Move given_up goals to evar_map
Diffstat (limited to 'tactics/class_tactics.ml')
| -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 |