From: Stefano Zacchiroli Date: Thu, 16 Jun 2005 15:11:56 +0000 (+0000) Subject: added depth and width (optional) parameters to auto_tac_new X-Git-Tag: INDEXING_NO_PROOFS~130 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7db8899532352e046abea679641d0c77f470af01;p=helm.git added depth and width (optional) parameters to auto_tac_new --- diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index bf9ade7b1..7f6be1d9b 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -500,8 +500,12 @@ and auto_new_aux dbd width already_seen_goals = function end ;; +let default_depth = 5 +let default_width = 3 -let auto_tac_new ~(dbd:Mysql.dbd) = +let auto_tac_new ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) + () += let auto_tac dbd (proof,goal) = Hashtbl.clear inspected_goals; debug_print "Entro in Auto"; diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli index 4095457ae..14627a4a3 100644 --- a/helm/ocaml/tactics/autoTactic.mli +++ b/helm/ocaml/tactics/autoTactic.mli @@ -25,4 +25,8 @@ *) val auto_tac : ?num:int option -> Mysql.dbd -> ProofEngineTypes.tactic -val auto_tac_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic + +val auto_tac_new: + ?depth:int -> ?width:int -> dbd:Mysql.dbd -> unit -> + ProofEngineTypes.tactic + diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index ae9746da1..8938b99f3 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -3,7 +3,9 @@ val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic val auto : ?num:int option -> Mysql.dbd -> ProofEngineTypes.tactic -val auto_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic +val auto_new : + ?depth:int -> + ?width:int -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic val compare : term:Cic.term -> ProofEngineTypes.tactic val constructor : n:int -> ProofEngineTypes.tactic