added homepage URL, now we have one

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index be02d8c1b83eb552523a7a5425e3cb267010299c..4e222fd6ad6caf4795eb42d138c5964bb07b32cd 100644 (file)
--- 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