aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_notation.ml
AgeCommit message (Expand)Author
2018-11-28Factor out common code in numeral/string notationsJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross