From c48117086c36e328d37a0400a4bda72d1537554f Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 26 Apr 2008 08:26:20 +0000
Subject: 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
---
 tactics/class_tactics.ml4 | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'tactics')

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 = 
-- 
cgit v1.2.3