X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTypes.mli;h=306c42daa75c22c73af7b52a399def3cfac19b67;hb=eeed0d603ddadba6b5ee5041e87794051b9283dd;hp=5014f41ce10d6eb75c60a6b2ec1a768cf5120ae0;hpb=c0a3562da676a9eb5dba565af89a3261a8c40363;p=helm.git diff --git a/helm/software/components/tactics/autoTypes.mli b/helm/software/components/tactics/autoTypes.mli index 5014f41ce..306c42daa 100644 --- a/helm/software/components/tactics/autoTypes.mli +++ b/helm/software/components/tactics/autoTypes.mli @@ -25,7 +25,9 @@ type flags = { maxwidth: int; + maxsize: int; maxdepth: int; + maxgoalsizefactor : int; timeout: float; use_library: bool; use_paramod: bool; @@ -39,8 +41,8 @@ val default_flags : unit -> flags (* (metasenv, subst, (metano,depth)list *) type sort = P | T;; type and_elem = - Cic.metasenv * Cic.substitution * (ProofEngineTypes.goal * int * sort) list + (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * (ProofEngineTypes.goal * int * sort) list type auto_result = | Fail of string - | Success of Cic.metasenv * Cic.substitution * and_elem list + | Success of (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * and_elem list