aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/number.ml
AgeCommit message (Expand)Author
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2020-11-05Merge numeral and string notation pluginsPierre Roux