fixed proofs, contextualization should now work.

[helm.git] / components / tactics / autoTactic.ml

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index 7aabf9f3378321e8de1e1737d17afef25d421329..a9505d73919f1d33a929599b5741c59a930f4efb 100644 (file)
--- a/components/tactics/autoTactic.ml
+++ b/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