aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorEnrico Tassi2015-07-01 11:25:47 +0200
committerEnrico Tassi2015-07-01 11:25:55 +0200
commit0917ce7cf48cadacc6fca48ba18b395740cccbe2 (patch)
tree883b3c7e087e8791fbe8cf5c2bbf2b2676f34013 /kernel/cbytecodes.ml
parent72f128af5a00e5509239e46b395c9cd10e53b36a (diff)
Notation: use same level for "@" in constr: and pattern: (Close: #4272)
A possible script breakage can occur if one has a notation at level 11 that is also right associative (now 11 is left associative). Thanks Georges for debugging that.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions