aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_notation.ml
AgeCommit message (Expand)Author
2020-11-04[numeral notation] Add a pre/postprocessingPierre Roux
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-24Use global env in numeral and string notationsMaxime Dénès
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2018-11-28Factor out common code in numeral/string notationsJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross