diff options
| author | Hugo Herbelin | 2018-07-20 23:37:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-02 13:18:14 +0200 |
| commit | 75f5e200f4f7eb6ca829869a8f8dada45e9751e9 (patch) | |
| tree | 033d58b65bb24a2cef81fea1ff4e0d60a67930f3 /kernel/nativecode.ml | |
| parent | 6f1c4ac389e595e09fdf4653847d8c3ccca0befb (diff) | |
Fixing #8106 (anomaly if declaring levels for only printing then only parsing).
Notations were not initially designed to support independent parsing
and printing rules. Some redesign of this part of the code shall be
necessary at some time.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions