diff options
| author | Hugo Herbelin | 2019-11-12 09:52:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-19 20:45:23 +0100 |
| commit | 7e3d008dc3ac001e0630bcaf8d4ec87f8a0006df (patch) | |
| tree | ed22a7f8f5a1073e75d265dbca64eeb9fa71d56f /kernel/nativelambda.mli | |
| parent | e7b29adca3c2ff636ff277dab843d517894f3bf6 (diff) | |
Grammar: slight simplification of treatment of annot/binder overlapping.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions