type flags = {
maxwidth: int;
+ maxsize: int;
maxdepth: int;
+ maxgoalsizefactor : int;
timeout: float;
+ use_library: bool;
use_paramod: bool;
use_only_paramod : bool;
+ close_more : bool;
dont_cache_failures: bool;
+ do_types: bool;
}
let default_flags _ =
- {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +.
- 3.0;use_paramod=true;use_only_paramod=false;dont_cache_failures=false}
+ {maxwidth=3;
+ maxdepth=3;
+ maxsize = 6;
+ maxgoalsizefactor = max_int;
+ timeout=Unix.gettimeofday() +.3.0;
+ use_library=false;
+ use_paramod=true;
+ use_only_paramod=false;
+ close_more=false;
+ dont_cache_failures=false;
+ do_types=false;
+}
;;
(* (metasenv, subst, (metano,depth)list *)
type sort = P | T;;
-type and_elem = Cic.metasenv * Cic.substitution * (int * int * sort) list
+type and_elem = (int * Cic.term * Cic.term) * Cic.metasenv * Cic.substitution * (int * 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