diff options
| author | Hugo Herbelin | 2017-08-17 20:12:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:06 +0100 |
| commit | e4d93d1cef27d3a8c1e36139fc1e118730406f67 (patch) | |
| tree | 0149d4c6ff1fc4cc978e796f303ee6dcdda65074 /kernel/type_errors.ml | |
| parent | 50970e4043d73d9a4fbd17ffe765745f6d726317 (diff) | |
Adding general support for irrefutable disjunctive patterns.
This now works not only for parsing of fun/forall (as in 8.6), but
also for arbitraty notations with binders and for printing.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions