diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-30 11:41:29 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-30 11:41:29 +0000 |
| commit | 1c40b709c43a2dbe9391ed229ca5aa4ac01658af (patch) | |
| tree | ea70310a5c3817b3cfa18db7699480ef6529b9f2 /tactics | |
| parent | 4862093dcb9a6335e70a290360748faf16946740 (diff) | |
Correct a bug in "new auto" and also unify_eqn which did not do local
delta conversion when it should (setoid_rewrite bug reported by
roconnor).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10874 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 2c327b71b..949db0e0f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -856,7 +856,7 @@ let delta_full_auto mod_delta n lems gl = let dbnames = list_subtract dbnames ["v62"] in let db_list = List.map (fun x -> searchtable_map x) dbnames in let hyps = pf_hyps gl in - tclTRY (search n false db_list (make_local_hint_db false lems gl) hyps) gl + tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl) hyps) gl let full_auto = delta_full_auto false let new_full_auto = delta_full_auto true diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 4319a1d3d..774e03c2c 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -643,7 +643,7 @@ let rewrite2_unif_flags = { } let convertible env evd x y = - Reductionops.is_trans_conv conv_transparent_state env (Evd.evars_of evd) x y + Reductionops.is_conv env (Evd.evars_of evd) x y let allowK = true |