diff options
| author | Hugo Herbelin | 2020-02-15 08:49:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-16 21:44:43 +0100 |
| commit | 96e78e7e25d666f30a7c00e0288762e127690c67 (patch) | |
| tree | 8fdf7f66fd76ae87778300697420fa8cd177358a /kernel/type_errors.mli | |
| parent | 29919b725262dca76708192bde65ce82860747be (diff) | |
Suite picking numeral notation
Ceci est une suite à numeral notation in custom entries, cherchant à
raffiner la compatibilité entre entrées. C'est mélangé avec le "pick"
précédent, et c'est en chantier.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions