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;
+ skip_trie_filtering: bool;
+ skip_context: bool;
}
let default_flags _ =
{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}
+ dont_cache_failures=false;
+ do_types=false;
+ skip_trie_filtering=false;
+ skip_context=false;
+}
;;
(* (metasenv, subst, (metano,depth)list *)