aboutsummaryrefslogtreecommitdiff
path: root/vernac/egramcoq.mli
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-22Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-07-29Store marshallable data in the custom entry summary.Pierre-Marie Pédrot
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-27[api] [parsing] Move Egram* to `vernac/`Emilio Jesus Gallego Arias