diff options
| author | Hugo Herbelin | 2020-09-02 17:27:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 17:25:16 +0100 |
| commit | 55389f1a1705b5c548161e1e5cc3eb5e34dda41d (patch) | |
| tree | 8340285f440aa45eeaa4fb3f8ca56cbfd7ad1a6d /kernel/nativelambda.mli | |
| parent | cd8aefceb03effbda979ea7403c20eaa7ca4cef7 (diff) | |
Using labels to document match_notation_constr.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions