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