X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=4e222fd6ad6caf4795eb42d138c5964bb07b32cd;hb=b9af9f1c0de6a1735b492f5c793a87a8fce218cc;hp=be02d8c1b83eb552523a7a5425e3cb267010299c;hpb=cb983fed69f0d209e19e22f3abcac5041f5f4a63;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index be02d8c1b..4e222fd6a 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -169,7 +169,7 @@ let rec find_matches metasenv context ugraph lift_amount term =
                 let t2 = Unix.gettimeofday () in
                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
                 r
-              with e ->
+              with Inference.MatchingFailure as e ->
                 let t2 = Unix.gettimeofday () in
                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
                 raise e
@@ -184,10 +184,13 @@ let rec find_matches metasenv context ugraph lift_amount term =
           if o <> U.Incomparable then
             try
               do_match c other eq_URI
-            with e ->
+            with Inference.MatchingFailure ->
               find_matches metasenv context ugraph lift_amount term tl
           else
-            let res = try do_match c other eq_URI with e -> None in
+            let res =
+              try do_match c other eq_URI
+              with Inference.MatchingFailure -> None
+            in
             match res with
             | Some (_, s, _, _, _) ->
                 let c' = (* M. *)apply_subst s c
@@ -237,7 +240,10 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
                 let t2 = Unix.gettimeofday () in
                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
                 r
-              with e ->
+              with
+              | Inference.MatchingFailure
+              | CicUnification.UnificationFailure _
+              | CicUnification.Uncertain _ as e ->
                 let t2 = Unix.gettimeofday () in
                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
                 raise e
@@ -254,7 +260,10 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
               let res = do_match c other eq_URI in
               res::(find_all_matches ~unif_fun metasenv context ugraph
                       lift_amount term tl)
-            with e ->
+            with
+            | Inference.MatchingFailure
+            | CicUnification.UnificationFailure _
+            | CicUnification.Uncertain _ ->
               find_all_matches ~unif_fun metasenv context ugraph
                 lift_amount term tl
           else
@@ -272,9 +281,12 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
                   else
                     find_all_matches ~unif_fun metasenv context ugraph
                       lift_amount term tl
-            with e ->
-              find_all_matches ~unif_fun metasenv context ugraph
-                lift_amount term tl
+            with
+            | Inference.MatchingFailure
+            | CicUnification.UnificationFailure _
+            | CicUnification.Uncertain _ ->
+                find_all_matches ~unif_fun metasenv context ugraph
+                  lift_amount term tl
 ;;
 
 
@@ -314,13 +326,13 @@ let subsumption env table target =
           let t2 = Unix.gettimeofday () in
           match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
           r
-        with e ->
+        with Inference.MatchingFailure as e ->
           let t2 = Unix.gettimeofday () in
           match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
           raise e
       in
       samesubst subst subst'
-    with e ->
+    with Inference.MatchingFailure ->
       false
   in
   let r = List.exists (ok right) leftr in