diff options
| author | Hugo Herbelin | 2020-07-29 09:53:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-25 22:27:31 +0200 |
| commit | 324e647cb9372dff2c12088524d8371fa3c1cd85 (patch) | |
| tree | 57b078e1381d41c56e19b771c50d1cc484dfe910 /parsing/extend.ml | |
| parent | 51c0d56a5b0384e2f6bd980a1111547641c66b3e (diff) | |
A fix and two enhancements of trailing pattern factorization in rec. notations.
The fix is a missing check of equality of custom entries. The enhancements are:
- not to bother breaking hints
- not to care about the border or internal position when the level is
made explicit
Ideally, one could also improve the treatment of DefaultLevel. To be
done later on.
Diffstat (limited to 'parsing/extend.ml')
0 files changed, 0 insertions, 0 deletions