X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=b232d9894c444fb1ea2b431ff3811908e033930f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=9b716637a9ed8c0c1c4ba2736034595365b461b3;hpb=9547c888a55a5372ff2f6a2d2a9eab7d5d7c01fb;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 9b716637a..b232d9894 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -306,7 +306,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
 
 let paramodulation_tactic = ref
   (fun dbd ?full ?depth ?width status ->
-     raise (ProofEngineTypes.Fail "Not Ready yet..."));;
+     raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
 
 let term_is_equality = ref
   (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
@@ -325,7 +325,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
         auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)]
       with
         [] ->  debug_print(lazy "Auto failed");
-	  raise (ProofEngineTypes.Fail "No Applicable theorem")
+	  raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
       | (_,(proof,[],_))::_ ->
           let t2 = Unix.gettimeofday () in
 	  debug_print (lazy "AUTO_TAC HA FINITO");