diff options
Diffstat (limited to 'contrib/interface/blast.ml')
| -rw-r--r-- | contrib/interface/blast.ml | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 6ec0fac4..767a7dd6 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -161,21 +161,22 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (add_hint_list hintl local_db) g'))) :: + (Hint_db.add_list hintl local_db) g'))) :: (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in - let flags = Auto.auto_unif_flags in let hintl = if occur_existential concl then - list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) - (Hint_db.map_all hdc db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in + List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) - (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in + List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in let tac_of_hint = fun (st, ({pri=b; pat = p; code=t} as _patac)) -> @@ -279,7 +280,7 @@ module MySearchProblem = struct let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') in - let ldb = add_hint_list hintl (List.hd s.localdb) in + let ldb = Hint_db.add_list hintl (List.hd s.localdb) in { depth = s.depth; tacres = res; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb }) @@ -375,7 +376,7 @@ let rec trivial_fail_db db_list local_db gl = tclTHEN intro (fun g'-> let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') - in trivial_fail_db db_list (add_hint_list hintl local_db) g') + in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g') in tclFIRST (assumption::intro_tac:: @@ -383,14 +384,15 @@ let rec trivial_fail_db db_list local_db gl = (trivial_resolve db_list local_db (pf_concl gl)))) gl and my_find_search db_list local_db hdc concl = - let flags = Auto.auto_unif_flags in let tacl = if occur_existential concl then - list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) - (Hint_db.map_all hdc db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in + List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) - (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in + List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in List.map (fun (st, {pri=b; pat=p; code=t} as _patac) -> @@ -477,7 +479,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal = with Failure _ -> [] in (free_try - (search_gen decomp n db_list (add_hint_list hintl local_db) [d]) + (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d]) g')) in let rec_tacs = |