aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/NotationDeprecation.v
AgeCommit message (Expand)Author
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès