diff options
| author | Pierre Letouzey | 2018-03-14 11:17:50 +0100 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:52 -0400 |
| commit | fa8e58f00b6774ac8669a7282d7863f8a605abd2 (patch) | |
| tree | c94f7bb1a07292f652f094007e1c51edbd73696c /interp/notation.mli | |
| parent | 64cb952f3fcf41c25a66a92bd124bba82e6db3f6 (diff) | |
Notation: avoid one intermediate (unit -> ...)
Diffstat (limited to 'interp/notation.mli')
0 files changed, 0 insertions, 0 deletions