aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/StringSyntax.v
AgeCommit message (Expand)Author
2020-11-05Allow multiple primitive notation on the same scope and triggersPierre Roux
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2018-11-28Add a couple more printing tests for byte/asciiJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross