diff options
| author | Hugo Herbelin | 2019-12-25 14:00:16 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-15 22:23:08 +0100 |
| commit | af8ddf0038e0caac1763da7ef510e4d5fdd4b8e7 (patch) | |
| tree | 1739d127ac013589739f61723d19cd45cd855ca8 /plugins/syntax/float_syntax.ml | |
| parent | 44ec3c8fd02f27d1dc7123bfbe5f5018937d6b86 (diff) | |
Fixing a precedence printing bug with custom entries.
Insertion of coercion to manage precedence of custom entries are
treated in constrextern.ml, while ppconstr.ml is only about the
management of precedences for constr.
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions