From 577cd769f88edc9aa851f117df7f83909c95a06c Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 21 Jul 2005 20:34:55 +0000
Subject: [PATCH] if paramodulation fails, go on with the normal auto...

---
 helm/ocaml/tactics/autoTactic.ml | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index d46aa6949..72609b118 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -310,18 +310,7 @@ let term_is_equality = ref
 
 let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () =
   let auto_tac dbd (proof, goal) =
-    let paramodulation_ok =
-      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
-        !paramodulation_tactic dbd (proof, goal)
-      with e ->
-        raise (ProofEngineTypes.Fail "paramodulation failure")
-    ) else
+    let normal_auto () = 
       let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
       Hashtbl.clear inspected_goals;
       debug_print "Entro in Auto";
@@ -340,6 +329,20 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () =
           debug_print (Printf.sprintf "tempo: %.9f\n" (t2 -. t1));
 	  (proof,[])
       | _ -> assert false
+    in
+    let paramodulation_ok =
+      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
+        !paramodulation_tactic dbd (proof, goal)
+      with e ->
+        normal_auto ()
+    ) else
+      normal_auto () 
   in
   ProofEngineTypes.mk_tactic (auto_tac dbd)
 ;;
-- 
2.39.2