diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-31 21:19:22 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-31 21:19:22 +0000 |
| commit | 30f6fd59780f57201e93ef4986422b6c89077ab4 (patch) | |
| tree | dd99fe7beae18eaaec8bf19d38f8aae97877078f /plugins/subtac/subtac_coercion.ml | |
| 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 'plugins/subtac/subtac_coercion.ml')
| -rw-r--r-- | plugins/subtac/subtac_coercion.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index d09ab4312..a1159dcaa 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -408,10 +408,10 @@ module Coercion = struct else let v', t' = try - let t2,t1,p = lookup_path_between env ( evd) (t,c1) in + let t2,t1,p = lookup_path_between env evd (t,c1) in match v with Some v -> - let j = apply_coercion env ( evd) p + let j = apply_coercion env evd p {uj_val = v; uj_type = t} t2 in Some j.uj_val, j.uj_type | None -> None, t @@ -427,8 +427,8 @@ module Coercion = struct try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match - kind_of_term (whd_betadeltaiota env ( evd) t), - kind_of_term (whd_betadeltaiota env ( evd) c1) + kind_of_term (whd_betadeltaiota env evd t), + kind_of_term (whd_betadeltaiota env evd c1) with | Prod (name,t1,t2), Prod (_,u1,u2) -> (* Conversion did not work, we may succeed with a coercion. *) |