X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=a9505d73919f1d33a929599b5741c59a930f4efb;hb=abd976fb6603a85c1da6d1582114e7c1fa472449;hp=9db6ed1c9094d3816c374592d401d5ba35fcdd7f;hpb=a060ed37101ce0e97bc26af8d49ce2491471c60c;p=helm.git

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 9db6ed1c9..a9505d739 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -339,7 +339,14 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
     if paramodulation_ok then (
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
-      Saturation.saturate dbd ~depth ~width ~full (proof, goal)
+      try
+        let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in
+        prerr_endline (Saturation.get_stats ());
+        rc
+      with exn ->
+        prerr_endline (Saturation.get_stats ());
+        raise exn
+      
 (*       with ProofEngineTypes.Fail _ -> *)
 (*         normal_auto () *)
     ) else