`deprecated` attribute support for notations and syntactic definitions

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.

1 files changed, 62 insertions, 0 deletions

diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v
new file mode 100644
index 0000000000..d313ba0aa4
--- /dev/null
+++ b/test-suite/success/NotationDeprecation.v
@@ -0,0 +1,62 @@
+Module Syndefs.
+
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation foo := Prop.
+
+Notation bar := Prop (compat "8.8").
+
+Fail
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation zar := Prop (compat "8.8").
+
+Check foo.
+Check bar.
+
+Set Warnings "+deprecated".
+
+Fail Check foo.
+Fail Check bar.
+
+End Syndefs.
+
+Module Notations.
+
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation "!!" := Prop.
+
+Notation "##" := Prop (compat "8.8").
+
+Fail
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation "**" := Prop (compat "8.8").
+
+Check !!.
+Check ##.
+
+Set Warnings "+deprecated".
+
+Fail Check !!.
+Fail Check ##.
+
+End Notations.
+
+Module Infix.
+
+#[deprecated(since = "8.8", note = "Do not use.")]
+Infix "!!" := plus (at level 1).
+
+Infix "##" := plus (at level 1, compat "8.8").
+
+Fail
+#[deprecated(since = "8.8", note = "Do not use.")]
+Infix "**" := plus (at level 1, compat "8.8").
+
+Check (_ !! _).
+Check (_ ## _).
+
+Set Warnings "+deprecated".
+
+Fail Check (_ !! _).
+Fail Check (_ ## _).
+
+End Infix.