diff options
| author | Hugo Herbelin | 2019-11-13 23:36:59 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-30 18:59:26 +0100 |
| commit | a71fa32802d05bfe63263730c40e93015bb71f8b (patch) | |
| tree | 97cb821cf1908e882da34bf4dbc4d4dee0fe620f /kernel/type_errors.ml | |
| parent | d3e97ef2b9c631ab4eccb867ea68cddc9a389939 (diff) | |
Refactoring code for matching partial applications against notations.
Should be semantically equivalent.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions