diff options
| author | Hugo Herbelin | 2017-09-25 18:01:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-25 18:01:54 +0200 |
| commit | b789106117653fec8340ecbd88866c254fe1201d (patch) | |
| tree | 771b93379ebe49a3ff46dbbf1a7b80c73d6f7931 /dev/base_include | |
| parent | 06a723190858da8ed3f30736f22398aa7822c959 (diff) | |
Fixing a little parsing bug with level 90 introduced in 3e70ea9c.
Unfortunately, some manual synchronization is needed between the
constr parser and the table of constr/pattern levels.
We do this synchronization which was missing in the commit moving
"x -> y" to a user-level notation.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions