aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppextend.mli
AgeCommit message (Expand)Author
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias