Removed several try .... with _ -> (which make thread killing impossible ;-((

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 84eaa2559ae383a3d83f9de0b36d8998aba7e985..16be77edb443c84c3c7845182564dacfb1601cce 100644 (file)
--- 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 054ad98bd5bd2e779d254179673c7fe58532cb25..d09eacc49773a2a655db35a2d545e47c5a9bb975 100644 (file)
--- 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 1319c13ca2dc34fa1e20299f0be540fab22c6df0..d499acb9ad2cb8a1ed70119d05a6c629f659edc0 100644 (file)
--- 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: " ^