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

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

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index fe3cf09f14c5e02e047ddb18e839c3f76a3dbf43..c0a7ec61180450d9e1633f4001bac144d7fbdc38 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -2051,12 +2051,12 @@ let saturate
           debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
           debug_print (lazy (CicPp.pp proof names));
           raise (ProofEngineTypes.Fail
-                   "Found a proof, but it doesn't typecheck")
+                  (lazy "Found a proof, but it doesn't typecheck"))
       in
       debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
       newstatus          
   | _ ->
-      raise (ProofEngineTypes.Fail "NO proof found")
+      raise (ProofEngineTypes.Fail (lazy "NO proof found"))
 ;;
 
 (* dummy function called within matita to trigger linkage *)