chore: remove bootstrapping workaround (#10484)

This PR removes temporary bootstrapping workarounds introduced in PR
#10479.

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.

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}) <|

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
 /--