aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/number.ml
AgeCommit message (Expand)Author
2021-02-27Remove decimal-only number notationsPierre Roux
2021-02-26Signed primitive integersAna
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2020-11-05Merge numeral and string notation pluginsPierre Roux