diff options
| author | Hugo Herbelin | 2020-05-14 07:24:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-14 07:45:23 +0200 |
| commit | 6a85fd439ed9051d0ae87fe134d223ccd1bd94ae (patch) | |
| tree | 3627b591d2c80278997f5a4c150c9f995c7e8dc6 /plugins | |
| parent | 91b5990e724acc863a5dba66acc33fd698ac26f0 (diff) | |
Fixes #12322 (anomaly when printing "fun" binders with implicit types).
A pattern-matching clause was missing in 5f314036e4d (PR #11261).
The anomaly triggered in configurations like "fun (x:T) y => ..."
(even in the absence of "Implicit Types").
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions