diff options
| author | herbelin | 2010-10-31 21:19:22 +0000 |
|---|---|---|
| committer | herbelin | 2010-10-31 21:19:22 +0000 |
| commit | 30f6fd59780f57201e93ef4986422b6c89077ab4 (patch) | |
| tree | dd99fe7beae18eaaec8bf19d38f8aae97877078f /tactics | |
| parent | f35a2ddd119ca99e924c68e3346a07087811c261 (diff) | |
Cleaning the use of parentheses around evd and evdref (cosmetic commit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13597 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index eca7c16f35..99cbfe4980 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1497,7 +1497,7 @@ let unification_rewrite l2r c1 c2 cl car rel but gl = let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' in let cl' = {cl with evd = evd'} in let cl' = Clenvtac.clenv_pose_dependent_evars true cl' in - let nf c = Evarutil.nf_evar ( cl'.evd) (Clenv.clenv_nf_meta cl' c) in + let nf c = Evarutil.nf_evar cl'.evd (Clenv.clenv_nf_meta cl' c) 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 |