diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-15 18:17:12 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-02-15 18:17:12 +0000 |
| commit | a365fc714c0303630cbfedcffc182b1fbeda0173 (patch) | |
| tree | c8602b2b1786e90e73ed843cd6039c44674e8f32 /plugins/subtac/subtac_coercion.ml | |
| parent | 22be25d786f4c4fae9c314ac7d774334e2a8a42b (diff) | |
Avoid unnecessary normalizations w.r.t. evars in Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14981 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac/subtac_coercion.ml')
| -rw-r--r-- | plugins/subtac/subtac_coercion.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 7e57c51ae..83555716d 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -110,7 +110,6 @@ module Coercion = struct and coerce loc env isevars (x : Term.constr) (y : Term.constr) : (Term.constr -> Term.constr) option = - let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in let rec coerce_unify env x y = let x = hnf env isevars x and y = hnf env isevars y in try @@ -383,7 +382,7 @@ module Coercion = struct try let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in let j1 = apply_coercion env ( isevars) p j t in - (isevars,type_judgment env (j_nf_evar ( isevars) j1)) + (isevars, type_judgment env (j_nf_evar ( isevars) j1)) with Not_found -> error_not_a_type_loc loc env ( isevars) j @@ -467,8 +466,7 @@ module Coercion = struct let (evd', val') = try inh_conv_coerce_to_fail loc env evd rigidonly - (Some (nf_evar evd cj.uj_val)) - (nf_evar evd cj.uj_type) (nf_evar evd t) + (Some cj.uj_val) cj.uj_type t with NoCoercion -> let sigma = evd in try |