diff options
| author | Assia Mahboubi | 2018-08-30 15:41:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-11 11:55:51 +0200 |
| commit | acedbd2b83913db24014539ab75b75bb0a64951f (patch) | |
| tree | b767dcbb6c9008ad7be1fc95ec664f90ce6983c2 /kernel/type_errors.ml | |
| parent | 2f0e274a1436b477e0be0be94a36ee9461a89767 (diff) | |
Grammar entry for the ssr syntax for anonymous arguments.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions