diff options
| author | herbelin | 2006-10-21 17:28:28 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-21 17:28:28 +0000 |
| commit | b5c3ab50b42bc9004dfa69d3e25a1ea9c5572986 (patch) | |
| tree | 2acd073d10dd594225aff872ddc8c211e32bd30a /pretyping/classops.ml | |
| 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/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 8f30f3fb82..49147dfd7a 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" |