aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/number.mli
AgeCommit message (Expand)Author
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05Merge numeral and string notation pluginsPierre Roux