This commit (partially) removes a big source of inefficiency (at least for

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 969d412cef43a28151e995250fdf10d2adc172c4..5ccd8741247ffa0a030893fa26ca9803342f08af 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -480,7 +480,7 @@ let unification_simple metasenv context t1 t2 ugraph =
     | C.Meta (i, _), C.Meta (j, _) when i > j ->
         unif subst menv t s
     | C.Meta _, t when occurs_check subst s t ->
-        raise (U.UnificationFailure "Inference.unification.unif")
+        raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
@@ -500,16 +500,16 @@ let unification_simple metasenv context t1 t2 ugraph =
       )
     | _, C.Meta _ -> unif subst menv t s
     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
-        raise (U.UnificationFailure "Inference.unification.unif")
+        raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
         try
           List.fold_left2
             (fun (subst', menv) s t -> unif subst' menv s t)
             (subst, menv) tls tlt
         with Invalid_argument _ ->
-          raise (U.UnificationFailure "Inference.unification.unif")
+          raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
       )
-    | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+    | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
   in
   let subst, menv = unif [] metasenv t1 t2 in
   let menv =