diff options
| author | Hugo Herbelin | 2017-11-26 19:18:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-27 11:27:34 +0100 |
| commit | 134b220b77d74b0ada801d215a2e5c66bc6726ea (patch) | |
| tree | 27889d694009730a3fd0db51587b95c725fa26c4 /API | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
Fixing associativity registered for level 10.
Apparently a long-standing bug, coupled with a pattern/constr
associativity inconsistency introduced while fixing another
pattern/constr level inconsistency (bug #4272, 0917ce7c).
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions