type flags = {
maxwidth: int;
+ maxsize: int;
maxdepth: int;
+ maxgoalsizefactor : int;
timeout: float;
+ use_library: bool;
use_paramod: bool;
use_only_paramod : bool;
- dont_cache_failures: bool
+ close_more : bool;
+ dont_cache_failures: bool;
+ do_types: bool;
}
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