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 /interp/notation.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 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions