added optional "paramodulation" parameter to auto to turn on paramodulation

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

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 72609b11842ac4f89e715eabdeba7ff714e6b19b..85c5c54be30300beb690e0d20a7c946afe11925a 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -308,7 +308,7 @@ let term_is_equality = ref
   (fun term -> debug_print "term_is_equality E` DUMMY!!!!"; false);;
 
 
-let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () =
+let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:Mysql.dbd) () =
   let auto_tac dbd (proof, goal) =
     let normal_auto () = 
       let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
@@ -331,16 +331,19 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () =
       | _ -> assert false
     in
     let paramodulation_ok =
-      let _, metasenv, _, _ = proof in
-      let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
-      !term_is_equality meta_goal
+      match paramodulation with
+      | None -> false
+      | Some _ ->
+          let _, metasenv, _, _ = proof in
+          let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
+          !term_is_equality meta_goal
     in
     if paramodulation_ok then (
       debug_print "USO PARAMODULATION...";
-      try
+(*       try *)
         !paramodulation_tactic dbd (proof, goal)
-      with e ->
-        normal_auto ()
+(*       with ProofEngineTypes.Fail _ -> *)
+(*         normal_auto () *)
     ) else
       normal_auto () 
   in