diff options
| author | filliatr | 1999-09-07 15:48:39 +0000 |
|---|---|---|
| committer | filliatr | 1999-09-07 15:48:39 +0000 |
| commit | a437f37c232847ce08b2862cb51ccf3cfc88569a (patch) | |
| tree | 784157b0686556cd668f76c3db9668da7099bf05 /kernel/type_errors.ml | |
| parent | be1e4a8b31b3082b6d70e77cce64c6515afcbfe7 (diff) | |
instanciation des opérateurs sur la bonne signature (celle de
définition, puisqu'elle ne peut pas changer, mais qu'elle peut être un
préfixe)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@45 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions