X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTypes.mli;h=5014f41ce10d6eb75c60a6b2ec1a768cf5120ae0;hb=631ef9768bce3958ca275cb7e5f0ff2de8e5e2a1;hp=c580bff3955849162e35785a6d0a77c16e339efb;hpb=beb4e1e9549d5b43e24907dc86c7ef899e487a3c;p=helm.git diff --git a/helm/software/components/tactics/autoTypes.mli b/helm/software/components/tactics/autoTypes.mli index c580bff39..5014f41ce 100644 --- a/helm/software/components/tactics/autoTypes.mli +++ b/helm/software/components/tactics/autoTypes.mli @@ -23,34 +23,18 @@ * http://cs.unibo.it/helm/. *) -type universe -val empty_universe:universe -val get_candidates: universe -> Cic.term -> Cic.term list -val universe_of_goals: - HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list -> - universe -> universe -val universe_of_context: Cic.context -> Cic.metasenv -> universe -> universe - -type cache -type cache_key = Cic.term -type cache_elem = - | Failed_in of int - | Succeded of Cic.term - | UnderInspection - | Notfound -val cache_examine: cache -> cache_key -> cache_elem -val cache_add_failure: cache -> cache_key -> int -> cache -val cache_add_success: cache -> cache_key -> Cic.term -> cache -val cache_add_underinspection: cache -> cache_key -> int -> cache -val cache_empty: cache - type flags = { maxwidth: int; maxdepth: int; timeout: float; + use_library: bool; + use_paramod: bool; + use_only_paramod : bool; + close_more : bool; + dont_cache_failures: bool } -val default_flags : flags +val default_flags : unit -> flags (* (metasenv, subst, (metano,depth)list *) type sort = P | T;;