aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/typeops.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-13 16:21:40 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-17 20:22:17 +0200
commit81ee9f1cb152a82cc4c116dd47294f2ae6eee0ed (patch)
tree223016d3593c18582e4523d93ed31f6a6977d7bd /checker/typeops.ml
parent57c6ffd23836364168ffd1c66dbddbecf830c7c6 (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 'checker/typeops.ml')
0 files changed, 0 insertions, 0 deletions