From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 29 May 2006 20:32:58 +0000 (+0000)
Subject: profilings are printed
X-Git-Tag: make_still_working~7297
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a5ae1f9778ff863f7124454008426d5bf7c0fd71;p=helm.git

profilings are printed
---

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 9db6ed1c9..7aabf9f33 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -339,7 +339,12 @@ 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
+        Saturation.saturate dbd ~depth ~width ~full (proof, goal)
+      with exn ->
+        prerr_endline (Saturation.get_stats ());
+        raise exn
+      
 (*       with ProofEngineTypes.Fail _ -> *)
 (*         normal_auto () *)
     ) else