diff options
| author | Hugo Herbelin | 2020-09-05 15:42:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-17 16:19:39 +0100 |
| commit | 2823c88d1dc1aa27e93217d5d3ad2e30155cd948 (patch) | |
| tree | 824c54000aca5e4792c7d9f231710c0087c3949d /kernel/type_errors.ml | |
| parent | 213207a1612d311f2f60d7e498ebd53a13ce039b (diff) | |
For printing, ordering notations by precision of the pattern.
This relies on finer-than partial order check with. In particular:
- number and order of notation metavariables does not matter
- take care of recursive patterns inclusion
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions