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;;