diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-26 08:26:20 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-26 08:26:20 +0000 |
| commit | c48117086c36e328d37a0400a4bda72d1537554f (patch) | |
| tree | c7c935abf43030f927132828e9a975a351777658 /tactics/class_tactics.ml4 | |
| parent | 87ce833c1b019ec7c25d151b26593f2f473f7554 (diff) | |
Debug implementation of failing tactics in Morphism to allow earlier
failures in proof search. Catch Refiner.FailError in typeclasses eauto
to indicate that an extern tactic failed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10853 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml4')
| -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 d6de5e69d..4319a1d3d 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 = |