aboutsummaryrefslogtreecommitdiff
path: root/interp/deprecation.mli
AgeCommit message (Collapse)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter.