2 files changed, 55 insertions, 0 deletions
diff --git a/test-suite/success/LtacDeprecation.v b/test-suite/success/LtacDeprecation.v
new file mode 100644
index 000000000..633a5e474
--- /dev/null
+++ b/test-suite/success/LtacDeprecation.v
@@ -0,0 +1,32 @@
+Set Warnings "+deprecated".
+
+#[deprecated(since = "8.8", note = "Use idtac instead")]
+Ltac foo x := idtac.
+
+Goal True.
+Fail (foo true).
+Abort.
+
+Fail Ltac bar := foo.
+Fail Tactic Notation "bar" := foo.
+
+#[deprecated(since = "8.8", note = "Use idtac instead")]
+Tactic Notation "bar" := idtac.
+
+Goal True.
+Fail bar.
+Abort.
+
+Fail Ltac zar := bar.
+
+Set Warnings "-deprecated".
+
+Ltac zar := foo.
+Ltac zarzar := bar.
+
+Set Warnings "+deprecated".
+
+Goal True.
+zar x.
+zarzar.
+Abort.
diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v
new file mode 100644
index 000000000..83fb3d0c8
--- /dev/null
+++ b/test-suite/success/attribute-syntax.v
@@ -0,0 +1,23 @@
+From Coq Require Program.
+
+Section Scope.
+
+#[local] Coercion nat_of_bool (b: bool) : nat :=
+  if b then 0 else 1.
+
+Check (refl_equal : true = 0 :> nat).
+
+End Scope.
+
+Fail Check 0 = true :> nat.
+
+#[polymorphic]
+Definition ι T (x: T) := x.
+
+Check ι _ ι.
+
+#[program]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+
+#[deprecated(since="8.9.0")]
+Ltac foo := foo.