X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=5ccd8741247ffa0a030893fa26ca9803342f08af;hb=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;hp=969d412cef43a28151e995250fdf10d2adc172c4;hpb=9e3eb63a93acaca0b4ad59c213e9ea430524d3ae;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 969d412ce..5ccd87412 100644
--- 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 =