From 30ad9beff172b797049b772e0a710c466c9ed18a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 16 Apr 2003 14:18:21 +0000
Subject: [PATCH] Removed several  try .... with _ -> (which make thread
 killing impossible ;-((

---
 helm/ocaml/tactics/proofEngineHelpers.ml |  3 +-
 helm/ocaml/tactics/tacticChaser.ml       | 94 ++++++++++++------------
 helm/ocaml/tactics/tacticals.ml          |  2 +-
 3 files changed, 49 insertions(+), 50 deletions(-)

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 84eaa2559..16be77edb 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -39,8 +39,7 @@ let mk_fresh_name context name ~typ =
            | C.Sort C.Set -> "x"
            | _ -> "H"
          )
-        with _ ->
-         "H"
+        with CicTypeChecker.TypeCheckerFailure _ -> "H"
        )
     | C.Name name ->
        Str.global_replace (Str.regexp "[0-9]*$") "" name
diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 054ad98bd..d09eacc49 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -51,52 +51,52 @@ let searchPattern ?(output_html = (fun _ -> ())) ~choose_must () ~status =
   let rigth_must = List.map torigth_restriction must in
   let rigth_only = Some (List.map torigth_restriction only) in
   let result =
-         MQueryGenerator.searchPattern
-          (rigth_must,[],[]) (rigth_only,None,None) in 
-        let uris =
-         List.map
-          (function uri,_ ->
-            MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
-          ) result in
-         let uris',exc =
-          let rec filter_out =
-           function
-              [] -> [],""
-            | uri::tl ->
-               let tl',exc = filter_out tl in
-                try
-                 if
-                  (try
-                   ignore
-                    (PrimitiveTactics.apply_tac
-                     ~term:(MQueryMisc.term_of_cic_textual_parser_uri
-                      (MQueryMisc.cic_textual_parser_uri_of_string uri))
-                     ~status);
-                   true
-                  with ProofEngineTypes.Fail _ -> false)
-                 then
-                  uri::tl',exc
-                 else
-                  tl',exc
-                with
-                 e ->
-                  let exc' =
-                   "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
-                    uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
-                  in
-                   tl',exc'
-          in
-           filter_out uris
-         in
-          let html' =
-           " <h1>Objects that can actually be applied: </h1> " ^
-           String.concat "<br>" uris' ^ exc ^
-           " <h1>Number of false matches: " ^
-            string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
-           " <h1>Number of good matches: " ^
-            string_of_int (List.length uris') ^ "</h1>"
-          in
-           output_html html' ;
-           uris'
+	 MQueryGenerator.searchPattern
+		(rigth_must,[],[]) (rigth_only,None,None) in 
+	let uris =
+	 List.map
+		(function uri,_ ->
+			MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
+		) result in
+	 let uris',exc =
+		let rec filter_out =
+		 function
+				[] -> [],""
+			| uri::tl ->
+				 let tl',exc = filter_out tl in
+					try
+					 if
+						(try
+						 ignore
+							(PrimitiveTactics.apply_tac
+							 ~term:(MQueryMisc.term_of_cic_textual_parser_uri
+								(MQueryMisc.cic_textual_parser_uri_of_string uri))
+							 ~status);
+						 true
+						with ProofEngineTypes.Fail _ -> false)
+					 then
+						uri::tl',exc
+					 else
+						tl',exc
+					with
+           (ProofEngineTypes.Fail _) as e ->
+						 let exc' =
+						  "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
+							 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
+						 in
+						  tl',exc'
+		in
+		 filter_out uris
+	 in
+		let html' =
+		 " <h1>Objects that can actually be applied: </h1> " ^
+		 String.concat "<br>" uris' ^ exc ^
+		 " <h1>Number of false matches: " ^
+			string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
+		 " <h1>Number of good matches: " ^
+			string_of_int (List.length uris') ^ "</h1>"
+		in
+		 output_html html' ;
+		 uris'
 ;;
 
diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 1319c13ca..d499acb9a 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -68,7 +68,7 @@ let rec try_tactics ~(tactics: (string * tactic) list) ~status =
         e ->
          match e with
             (Fail _)
-          | (CicTypeChecker.NotWellTyped _)
+          | (CicTypeChecker.TypeCheckerFailure (CicTypeChecker.NotWellTyped _))
           | (CicUnification.UnificationFailed) ->
               warn (
                 "Tacticals.try_tactics failed with exn: " ^
-- 
2.39.2