X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=e8d034a3298a9630fa0c8b1efe693579a1045ed2;hb=0582a602f0b1d6f5430326893a473d78b0aa7dfd;hp=8e94bba86e4f072796f32d482f363d5df2e5ed24;hpb=4cc970d00483c8c2a0a26cba3296bf855be01ed7;p=helm.git

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 8e94bba86..e8d034a32 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -317,22 +317,22 @@ let int params name default =
         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 ;;  
 
-let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
+let auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) =
   (* argument parsing *)
   let int = int params in
   let bool = bool params in
-  let newauto = bool "new" false in
+  let oldauto = bool "old" false in
   let use_only_paramod = bool "paramodulation" false in
-  let newauto = if use_only_paramod then true else newauto in
+  let oldauto = if use_only_paramod then false else oldauto in
   let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
   let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
-   if not newauto then 
+   if oldauto then 
     auto_tac_old ~depth ~width ~dbd () (proof,goal)
    else
-    ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params) (proof,goal)
+    ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params ~universe) (proof,goal)
 
-let auto_tac ~params ~dbd =
-      ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)
+let auto_tac ~params ~dbd ~universe=
+      ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe)
 ;;
 
 let pp_proofterm = Equality.pp_proofterm;;