Every exception that used to have type string is now a string Lazy.t.

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 003fb958430cf9597bc46909e06867c33db6018a..b9f165edb2d3c83ef3506357631d3228d0b49726 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -378,8 +378,7 @@ let unification_simple metasenv context t1 t2 ugraph =
         unif subst menv t s
     | C.Meta _, t when occurs_check subst s t ->
         raise
-          (U.UnificationFailure
-             (U.failure_msg_of_string "Inference.unification.unif"))
+          (U.UnificationFailure (lazy "Inference.unification.unif"))
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
@@ -400,20 +399,17 @@ 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
-                 (U.failure_msg_of_string "Inference.unification.unif"))
+        raise (U.UnificationFailure (lazy "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
-                   (U.failure_msg_of_string "Inference.unification.unif"))
+          raise (U.UnificationFailure (lazy "Inference.unification.unif"))
       )
     | _, _ ->
-        raise (U.UnificationFailure
-                 (U.failure_msg_of_string "Inference.unification.unif"))
+        raise (U.UnificationFailure (lazy "Inference.unification.unif"))
   in
   let subst, menv = unif [] metasenv t1 t2 in
   let menv =