diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index d6de5e69dd..4319a1d3de 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -161,6 +161,11 @@ let filter_hyp t = | Evar _ | Meta _ | Sort _ -> false | _ -> true +let rec catchable = function + | Refiner.FailError _ -> true + | Stdpp.Exc_located (_, e) -> catchable e + | e -> Logic.catchable_exception e + module SearchProblem = struct type state = search_state @@ -194,9 +199,7 @@ module SearchProblem = struct (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *) (* end; *) ((lgls,v'),pri,pptac) :: aux tacl - with e when Logic.catchable_exception e -> - (* if !debug then msg (str"failed\n"); *) - aux tacl + with e when catchable e -> aux tacl in aux l let nb_empty_evars s = |