aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/numeral.ml
AgeCommit message (Expand)Author
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-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2019-01-25[Numeral notations] Lazy resolution of decimal typesVincent Laporte
2019-01-25[Numeral notations] Use Coqlib registered constantsVincent Laporte
2018-11-28Factor out common code in numeral/string notationsJason Gross
2018-09-19Fix Numeral Notations (4/4 - fixing synch)Jason Gross
2018-09-19Fix Numeral Notations (3/4 - moving more stuff)Jason Gross
2018-09-19Fix Numeral Notations (2/4 - exceptions, usr_err)Jason Gross
2018-09-19Fix Numeral Notations (1/4 - moving things)Jason Gross
2018-08-31Make Numeral Notation obey Local/GlobalJason Gross
2018-08-31[numeral notations] support aliasesJason Gross
2018-08-31Add Numeral Notation GlobRef printing/parsingJason Gross
2018-08-31Add periods in response to PR commentsJason Gross
2018-08-31Move g_numeral.ml4 to numeral.mlJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:50:14 +0000