diff options
| author | herbelin | 2008-06-12 08:11:14 +0000 |
|---|---|---|
| committer | herbelin | 2008-06-12 08:11:14 +0000 |
| commit | 7a337e554e21f2943fa37f6ecee09e3b52be7772 (patch) | |
| tree | de5b003616122c688e1b42a89afd6b94a28fd1e9 /pretyping/typeclasses_errors.ml | |
| parent | 91d8c7eda69c2e97d73dbc2922f3ba92b03a2b2f (diff) | |
Confusion sur commit précédent de library. La capture du Not_found
dans la recherche du nom long était bien utile (parce que la table des
filename n'est plus synchronisée et plus dans le initial.coq) mais
c'est ailleurs qu'on reposait à tort sur la bonne synchronisation de
la table des noms longs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11111 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions