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 /pretyping/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 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 6cb32a8ad..f10fcbc2c 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -137,8 +137,8 @@ module Default = struct (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> let t,p = - lookup_path_to_fun_from env ( evd) j.uj_type in - (evd,apply_coercion env ( evd) p j t) + lookup_path_to_fun_from env evd j.uj_type in + (evd,apply_coercion env evd p j t) let inh_app_fun env evd j = try inh_app_fun env evd j @@ -148,15 +148,15 @@ module Default = struct let inh_tosort_force loc env evd j = try - let t,p = lookup_path_to_sort_from env ( evd) j.uj_type in - let j1 = apply_coercion env ( evd) p j t in - let j2 = on_judgment_type (whd_evar ( evd)) j1 in + let t,p = lookup_path_to_sort_from env evd j.uj_type in + let j1 = apply_coercion env evd p j t in + let j2 = on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env j2) with Not_found -> - error_not_a_type_loc loc env ( evd) j + error_not_a_type_loc loc env evd j let inh_coerce_to_sort loc env evd j = - let typ = whd_betadeltaiota env ( evd) j.uj_type in + let typ = whd_betadeltaiota env evd j.uj_type in match kind_of_term typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined_evar evd ev) -> |