diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 33 |
1 files changed, 13 insertions, 20 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3074c4c4..73fcd0ea 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Util open Names @@ -78,10 +78,6 @@ module Default = struct | App (f,l) -> mkApp (whd_evar sigma f,l) | _ -> whd_evar sigma t - let class_of1 env evd t = - let sigma = evars_of evd in - class_of env sigma (whd_app_evar sigma t) - (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = let rec apply_rec acc typ = function @@ -107,18 +103,16 @@ module Default = struct (* raise Not_found if no coercion found *) let inh_pattern_coerce_to loc pat ind1 ind2 = - let i1 = inductive_class_of ind1 in - let i2 = inductive_class_of ind2 in - let p = lookup_pattern_path_between (i1,i2) in + let p = lookup_pattern_path_between (ind1,ind2) in apply_pattern_coercion loc pat p (* appliquer le chemin de coercions p à hj *) - let apply_coercion env p hj typ_cl = + let apply_coercion env sigma p hj typ_cl = try fst (List.fold_left (fun (ja,typ_cl) i -> let fv,isid = coercion_value i in - let argl = (class_args_of typ_cl)@[ja.uj_val] in + let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in let jres = apply_coercion_args env argl fv in (if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } @@ -137,16 +131,15 @@ module Default = struct (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try - let t,i1 = class_of1 env evd j.uj_type in - let p = lookup_path_to_fun_from i1 in - (evd,apply_coercion env p j t) + let t,p = + lookup_path_to_fun_from env (evars_of evd) j.uj_type in + (evd,apply_coercion env (evars_of evd) p j t) with Not_found -> (evd,j)) let inh_tosort_force loc env evd j = try - let t,i1 = class_of1 env evd j.uj_type in - let p = lookup_path_to_sort_from i1 in - let j1 = apply_coercion env p j t in + let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in + let j1 = apply_coercion env (evars_of evd) p j t in let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in (evd,type_judgment env j2) with Not_found -> @@ -173,12 +166,12 @@ module Default = struct else let v', t' = try - let t1,i1 = class_of1 env evd c1 in - let t2,i2 = class_of1 env evd t in - let p = lookup_path_between (i2,i1) in + let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in match v with Some v -> - let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in + let j = + apply_coercion env (evars_of evd) p + {uj_val = v; uj_type = t} t2 in Some j.uj_val, j.uj_type | None -> None, t with Not_found -> raise NoCoercion |