From 34f5fba54dea20aecf6f01b33c6cf7382c6cc3d5 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Sun, 21 Sep 2025 09:36:49 +0200
Subject: [PATCH] chore: remove bootstrapping workaround (#10484)

This PR removes temporary bootstrapping workarounds introduced in PR
#10479.
---
 src/Init/Notation.lean        | 2 +-
 src/Lean/Elab/DocString.lean  | 3 ++-
 tests/lean/run/versoDocs.lean | 5 +----
 3 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index edb3d8ad94..ec4c4ddbef 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -855,7 +855,7 @@ which would include `#guard_msgs` itself, and would cause duplicate and/or uncap
 The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
 -/
 syntax (name := guardMsgsCmd)
-  (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
+  (plainDocComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
 
 /--
 Format and print the info trees for a given command.
diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean
index 70b80d3027..324c660c1c 100644
--- a/src/Lean/Elab/DocString.lean
+++ b/src/Lean/Elab/DocString.lean
@@ -1485,7 +1485,8 @@ private def elabModSnippet'
     if let `(block|header($n){$name*}) := b then
         let n := n.getNat
         if n > maxLevel then
-          logErrorAt b m!"Incorrect header nesting: expected at most `{"".pushn '#' n}`"
+          logErrorAt b m!"Incorrect header nesting: expected at most `{"#".pushn '#' maxLevel}` \
+            but got `{"#".pushn '#' n}`"
         else
           let title ←
             liftM <| withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := `no_elab, stx := b}) <|
diff --git a/tests/lean/run/versoDocs.lean b/tests/lean/run/versoDocs.lean
index 6df7bb1d6c..9e795c413b 100644
--- a/tests/lean/run/versoDocs.lean
+++ b/tests/lean/run/versoDocs.lean
@@ -204,14 +204,13 @@ def a := "a"
 def b := "b"
 end A
 
-/- Commented out for bootstrapping
 /-- error: Unknown constant `a` -/
 #guard_msgs in
 /--
 role {name}`a` here
 -/
 def testDef := 15
--/
+
 
 #guard_msgs in
 /--
@@ -229,7 +228,6 @@ def testDef' := 15
 -/
 def testDef'' := 15
 
-/- Commented out for bootstrapping
 /-- error: Unknown constant `b` -/
 #guard_msgs in
 /--
@@ -238,7 +236,6 @@ def testDef'' := 15
 {name}`b`
 -/
 def testDef''' := 15
--/
 
 #guard_msgs in
 /--