diff options
| author | msozeau | 2009-12-06 00:20:53 +0000 |
|---|---|---|
| committer | msozeau | 2009-12-06 00:20:53 +0000 |
| commit | 4cc4e14d6e34752c613d6701e5378708b219b242 (patch) | |
| tree | adea493acbf3e09f0bdb73b7b72b40baf20b2188 /tactics/rewrite.ml4 | |
| parent | 7533b5b51bfaa580fb237591b0fc747e0172526d (diff) | |
Fix anomaly when using typeclass resolution with filtered hyps in evars.
Make setoid_rewrite-through-rewrite's selection of occurences more
robust: do not try unification with reduction if not needed.
This changes a few scripts that were using reduction in a far from
obvious way and could break more.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12562 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 1ba25fc609..15ef2db2dc 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -334,7 +334,7 @@ let unify_eqn env sigma hypinfo t = let env', prf, c1, c2, car, rel = match abs with | Some (absprf, absprfty) -> - let env' = clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl in + let env' = clenv_unify allowK ~flags:rewrite_unif_flags CONV left t cl in env', prf, c1, c2, car, rel | None -> let env' = @@ -1370,7 +1370,9 @@ let unification_rewrite l2r c1 c2 cl car rel but gl = clenv_pose_metas_as_evars cl' mvs in let nf c = Evarutil.nf_evar ( cl'.evd) (Clenv.clenv_nf_meta cl' c) in - let c1 = nf c1 and c2 = nf c2 and car = nf car and rel = nf rel in + let c1 = if l2r then nf c' else nf c1 + and c2 = if l2r then nf c2 else nf c' + and car = nf car and rel = nf rel in check_evar_map_of_evars_defs cl'.evd; let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in |