diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-21 17:28:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-21 17:28:28 +0000 |
| commit | b5c3ab50b42bc9004dfa69d3e25a1ea9c5572986 (patch) | |
| tree | 2acd073d10dd594225aff872ddc8c211e32bd30a /pretyping | |
| parent | 76697fb3fd73564c06f7fee23e9a92c8f9da7664 (diff) | |
Le calcul de la classe dans class_args_of ne suivait pas celui de class_of
(avec comme conséquence des échecs en cas de beta-redex - cf coercions.v).
Allègements triviaux dans coercion.ml en passant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9257 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 2 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 14 |
2 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 8f30f3fb8..49147dfd7 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -208,7 +208,7 @@ let class_of env sigma t = let inductive_class_of ind = fst (class_info (CL_IND ind)) -let class_args_of c = snd (decompose_app c) +let class_args_of c = snd (find_class_type c) let string_of_class = function | CL_FUN -> "Funclass" diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 0460b4177..374f11543 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -72,7 +72,9 @@ module Default = struct | App (f,l) -> mkApp (whd_evar sigma f,l) | _ -> whd_evar sigma t - let class_of1 env sigma t = class_of env sigma (whd_app_evar sigma t) + let class_of1 env isevars t = + let sigma = evars_of isevars 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 = @@ -90,7 +92,6 @@ module Default = struct apply_rec [] funj.uj_type argl (* appliquer le chemin de coercions de patterns p *) - let apply_pattern_coercion loc pat p = List.fold_left (fun pat (co,n) -> @@ -106,7 +107,6 @@ module Default = struct apply_pattern_coercion loc pat p (* appliquer le chemin de coercions p à hj *) - let apply_coercion env p hj typ_cl = try fst (List.fold_left @@ -131,14 +131,14 @@ module Default = struct (isevars',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in + let t,i1 = class_of1 env isevars j.uj_type in let p = lookup_path_to_fun_from i1 in (isevars,apply_coercion env p j t) with Not_found -> (isevars,j)) let inh_tosort_force loc env isevars j = try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in + let t,i1 = class_of1 env isevars j.uj_type in let p = lookup_path_to_sort_from i1 in let j1 = apply_coercion env p j t in let j2 = on_judgment_type (whd_evar (evars_of isevars)) j1 in @@ -161,8 +161,8 @@ module Default = struct let inh_coerce_to_fail env isevars c1 v t = let v', t' = try - let t1,i1 = class_of1 env (evars_of isevars) c1 in - let t2,i2 = class_of1 env (evars_of isevars) t in + let t1,i1 = class_of1 env isevars c1 in + let t2,i2 = class_of1 env isevars t in let p = lookup_path_between (i2,i1) in match v with Some v -> |