X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=b232d9894c444fb1ea2b431ff3811908e033930f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e89608cd4f9c04438b3e1e7d2f823f5efeb11c64;hpb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index e89608cd4..b232d9894 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -279,7 +279,7 @@ let default_depth = 5
 let default_width = 3
 
 (*
-let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
+let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
   ()
 =
   let auto_tac dbd (proof,goal) =
@@ -305,13 +305,15 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
 *)
 
 let paramodulation_tactic = ref
-  (fun dbd status -> raise (ProofEngineTypes.Fail "Not Ready yet..."));;
+  (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 ~(dbd:Mysql.dbd) () =
+let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
+    ?full ~(dbd:HMysql.dbd) () =
   let auto_tac dbd (proof, goal) =
     let normal_auto () = 
       let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
@@ -323,7 +325,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd
         auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)]
       with
         [] ->  debug_print(lazy "Auto failed");
-	  raise (ProofEngineTypes.Fail "No Applicable theorem")
+	  raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
       | (_,(proof,[],_))::_ ->
           let t2 = Unix.gettimeofday () in
 	  debug_print (lazy "AUTO_TAC HA FINITO");
@@ -333,18 +335,19 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd
 	  (proof,[])
       | _ -> assert false
     in
+    let full = match full with None -> false | Some _ -> true in
     let paramodulation_ok =
       match paramodulation with
       | None -> false
       | Some _ ->
           let _, metasenv, _, _ = proof in
           let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
-          !term_is_equality meta_goal
+          full || (!term_is_equality meta_goal)
     in
     if paramodulation_ok then (
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
-        !paramodulation_tactic dbd (proof, goal)
+      !paramodulation_tactic dbd ~depth ~width ~full (proof, goal)
 (*       with ProofEngineTypes.Fail _ -> *)
 (*         normal_auto () *)
     ) else