diff options
| author | Hugo Herbelin | 2020-02-14 09:12:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-19 20:54:30 +0100 |
| commit | 9dc88f3c146aeaf8151fcef6ac45ca50675d052b (patch) | |
| tree | b11ae19ea90d594123049d501ddc21a50cee865f /interp/notation.ml | |
| parent | 1916fc22a187bdaaad4c99fa00f345c6f7314a73 (diff) | |
Only parsing in Reserved Notation: turning notice into a warning.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions