diff options
| author | Hugo Herbelin | 2016-10-13 16:21:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-17 20:22:17 +0200 |
| commit | 81ee9f1cb152a82cc4c116dd47294f2ae6eee0ed (patch) | |
| tree | 223016d3593c18582e4523d93ed31f6a6977d7bd /dev/include | |
| parent | 57c6ffd23836364168ffd1c66dbddbecf830c7c6 (diff) | |
Fixing a few other inconsistencies with notations.
`Notation ".a" := nat.' was accepted and used for printing but not
recognized in parsing. Now it does. Other examples in test-suite.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions