diff options
| author | Hugo Herbelin | 2017-10-28 20:07:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-10-28 20:26:46 +0200 |
| commit | de7d2fdb97975dcd94005bb6fa79a312c8afa017 (patch) | |
| tree | d2739984aa3f2090c17b9d18f884f1986c52dff0 /kernel/type_errors.ml | |
| parent | e5659c8ffe735c530a707a61c692a3af21a79a9a (diff) | |
Fixing #5401 (printing of patterns with bound anonymous variables).
This fixes also #5731, #6035, #5364.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions