let eq_uri = UriManager.strip_xpointer eq_uri in
let fake= Cic.Meta(-1,[]) in
let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
let eq_uri = UriManager.strip_xpointer eq_uri in
let fake= Cic.Meta(-1,[]) in
let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
let bool = bool params in
let close_more = bool "close_more" false in
let use_paramod = bool "use_paramod" true in
let bool = bool params in
let close_more = bool "close_more" false in
let use_paramod = bool "use_paramod" true in
AutoTypes.dont_cache_failures = false;
AutoTypes.maxgoalsizefactor = gsize;
AutoTypes.do_types = do_type;
AutoTypes.dont_cache_failures = false;
AutoTypes.maxgoalsizefactor = gsize;
AutoTypes.do_types = do_type;
let tables, elems, maxm =
List.fold_left
(fun (tables,elems,maxm) cand ->
let tables, elems, maxm =
List.fold_left
(fun (tables,elems,maxm) cand ->
in
let maxm = maxm1 in
elems@more_elems, tables, cache, maxm, flags
else
let elems, tables, cache, maxm =
applicative_case tables maxm depth s fake_proof goalno
in
let maxm = maxm1 in
elems@more_elems, tables, cache, maxm, flags
else
let elems, tables, cache, maxm =
applicative_case tables maxm depth s fake_proof goalno
in
elems, tables, cache, maxm, flags
;;
in
elems, tables, cache, maxm, flags
;;
let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) =
let _,metasenv,_subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) =
let _,metasenv,_subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let use_library = flags.use_library in
let tables,cache,newmeta =
let use_library = flags.use_library in
let tables,cache,newmeta =
false universe (proof, goal) in
let tables,cache,newmeta =
if flags.close_more then
false universe (proof, goal) in
let tables,cache,newmeta =
if flags.close_more then