Skip to content

Commit 02dfdf7

Browse files
authored
Merge pull request #2255 from Alizter/fix-warnings-in-test
chore: fix warnings in test/
2 parents 88577b8 + 4017dbe commit 02dfdf7

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

test/Tactics/napply.v

+4-4
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Fail Definition test1 : test1_type := ltac:(tapply exist).
1313
Succeed Definition test1 : test1_type := ltac:(napply exist; exact _).
1414

1515
(** Testing deprecated tactics *)
16-
Fail Definition test1 : test1_type := ltac:(nrapply exist).
17-
Fail Definition test1 : test1_type := ltac:(snrapply exist).
18-
19-
16+
Fail #[warnings="+deprecated-tactic-notation-since-2025-03-11"]
17+
Definition test1 : test1_type := ltac:(nrapply exist).
18+
Fail #[warnings="+deprecated-tactic-notation-since-2025-03-11"]
19+
Definition test1 : test1_type := ltac:(snrapply exist).

0 commit comments

Comments
 (0)