1 files changed, 32 insertions, 0 deletions
diff --git a/test-suite/success/LtacDeprecation.v b/test-suite/success/LtacDeprecation.v
new file mode 100644
index 00000000..633a5e47
--- /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.