let use_paramod = bool "use_paramod" true in
let use_only_paramod =
if for_applyS then true else bool "paramodulation" false in
let use_paramod = bool "use_paramod" true in
let use_only_paramod =
if for_applyS then true else bool "paramodulation" false in
let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
let timeout = int "timeout" 0 in
let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
let timeout = int "timeout" 0 in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let flags = flags_of_params params () in
(* just for testing *)
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let flags = flags_of_params params () in
(* just for testing *)
let tables,cache,newmeta =
init_cache_and_tables dbd use_library (proof, goal) in
let tables,cache,newmeta =
let tables,cache,newmeta =
init_cache_and_tables dbd use_library (proof, goal) in
let tables,cache,newmeta =
- close_more tables newmeta context (proof, goal) auto_all_solutions cache in
+ if flags.close_more then
+ close_more
+ tables newmeta context (proof, goal) auto_all_solutions cache
+ else tables,cache,newmeta in
let initial_time = Unix.gettimeofday() in
let (_,oldmetasenv,_,_) = proof in
let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
let initial_time = Unix.gettimeofday() in
let (_,oldmetasenv,_,_) = proof in
let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in