aboutsummaryrefslogtreecommitdiff
path: root/test-suite/interactive/PrimNotation.v
AgeCommit message (Expand)Author
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2018-08-31Update doc and test-suite after supporting univ polyJason Gross
2018-08-31WIP: adapt Numeral Notation to synchronized prim notationsPierre Letouzey
2018-08-31prim notations backtrackable, their declarations now in two parts (API change)Pierre Letouzey