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

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 7aabf9f33..a9505d739 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -340,7 +340,9 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
       try
-        Saturation.saturate dbd ~depth ~width ~full (proof, goal)
+        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