diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/firstorder/sequent.ml | 2 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/blast.ml | 30 | ||||
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 13 |
4 files changed, 26 insertions, 21 deletions
diff --git a/contrib/firstorder/sequent.ml b/contrib/firstorder/sequent.ml index e540058f14..fd5972fb74 100644 --- a/contrib/firstorder/sequent.ml +++ b/contrib/firstorder/sequent.ml @@ -281,7 +281,7 @@ let create_with_auto_hints l depth gl= searchtable_map dbname with Not_found-> error ("Firstorder: "^dbname^" : No such Hint database") in - Hint_db.iter g (snd hdb) in + Hint_db.iter g hdb in List.iter h l; !seqref diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 3d80bd0040..d7bcde69cb 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = false (true,5) [Lazy.force refl_equal] - [empty_transparent_state, Auto.Hint_db.empty] + [Auto.Hint_db.empty false] ) ) ) diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 6ec0fac42d..767a7dd667 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 = diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 474b3616a8..70087b2d44 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -452,11 +452,14 @@ let (theory_to_obj, obj_to_theory) = let setoid_of_relation env a r = - lapp coq_mk_Setoid - [|a ; r ; - Class_tactics.reflexive_proof env a r ; - Class_tactics.symmetric_proof env a r ; - Class_tactics.transitive_proof env a r |] + try + lapp coq_mk_Setoid + [|a ; r ; + Class_tactics.reflexive_proof env a r ; + Class_tactics.symmetric_proof env a r ; + Class_tactics.transitive_proof env a r |] + with Not_found -> + error "cannot find setoid relation" let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] |