aboutsummaryrefslogtreecommitdiff
path: root/parsing/notation_gram.ml
AgeCommit message (Expand)Author
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-31Multiple payload types in tokensPierre Roux
2019-03-31[parsing] Split Tok.t into Tok.t and Tok.patternEnrico Tassi
2018-11-27[gramlib] Minor cleanups:Emilio Jesus Gallego Arias
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias