X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoTactic.ml;h=7aabf9f3378321e8de1e1737d17afef25d421329;hb=2d18e445ab3f9f24787667e8d8ee562bd1cb64bc;hp=42df90768263b2749c30f9ff81c1c0dcf4f9b12c;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index 42df90768..7aabf9f33 100644
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -334,12 +334,17 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
       | Some _ ->
           let _, metasenv, _, _ = proof in
           let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
-          full || (Inference.term_is_equality meta_goal)
+          full || (Equality.term_is_equality meta_goal)
     in
     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