X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=42df90768263b2749c30f9ff81c1c0dcf4f9b12c;hb=91af0f7726bcfcd72229f19c239eabfda4532347;hp=dc5b8324c0779096bba15fd22b74fc7aa213cca5;hpb=aa0d60227b785da3355b31519ba11cb4fbd2c925;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index dc5b8324c..42df90768 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -295,13 +295,14 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
 ;;
 *)
 
+(*
 let paramodulation_tactic = ref
   (fun dbd ?full ?depth ?width status ->
      raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
 
 let term_is_equality = ref
   (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
-
+*)
 
 let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
     ?full ~(dbd:HMysql.dbd) () =
@@ -333,12 +334,12 @@ 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 || (!term_is_equality meta_goal)
+          full || (Inference.term_is_equality meta_goal)
     in
     if paramodulation_ok then (
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
-      !paramodulation_tactic dbd ~depth ~width ~full (proof, goal)
+      Saturation.saturate dbd ~depth ~width ~full (proof, goal)
 (*       with ProofEngineTypes.Fail _ -> *)
 (*         normal_auto () *)
     ) else