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;
Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
max_int max_int flags.timeout
with
| None, _,_,_ ->
raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
| Some (_,proof''''',_), active,passive,_ ->
Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
max_int max_int flags.timeout
with
| None, _,_,_ ->
raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
| Some (_,proof''''',_), active,passive,_ ->
proof''''',
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
proof''''',
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
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
try
let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in
let metasenv = [(0,context,ty)] in
try
let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in
let metasenv = [(0,context,ty)] in
- let fake_proof = None,metasenv,[] ,Cic.Meta(0,mk_irl context),ty,[] in
+ let fake_proof = None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] in
let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
(PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0)
in
let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
(PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0)
in