aboutsummaryrefslogtreecommitdiff
path: root/parsing/notgram_ops.ml
AgeCommit message (Expand)Author
2018-09-02Fixing #8106 (anomaly if declaring levels for only printing then only parsing).Hugo Herbelin
2018-07-29Renaming ETName and ETReference so as to fit the user-visible terminology.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias