fix

leanprover-community · Jan 25, 2025 · 28f9440 · 28f9440
1 parent 9148932
commit 28f9440
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean
@@ -513,7 +513,4 @@ These are particularly helpful for writing tests to the `MathlibTest` suite.
 :::tactic Lean.Parser.Tactic.failIfSuccess
 :::
 
-Finally, this is a command and not a tactic, but it is also essential for test files.
-
-:::tactic Lean.guardMsgsCmd
-:::
+Finally, `#guard_msgs` is a command and not a tactic, but it is also essential for test files.