diff --git a/src/Lean/BuiltinDocAttr.lean b/src/Lean/BuiltinDocAttr.lean
index 93f55edc3e..ab12c9cfed 100644
--- a/src/Lean/BuiltinDocAttr.lean
+++ b/src/Lean/BuiltinDocAttr.lean
@@ -5,12 +5,12 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Compiler.InitAttr
-import Lean.DocString
+import Lean.DocString.Extension
 
 namespace Lean
 
 def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
-  if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
+  if let some doc ← findSimpleDocString? (← getEnv) declName (includeBuiltin := false) then
     declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
   if let some declRanges ← findDeclarationRanges? declName then
     declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean
index 066d1e967a..d288228209 100644
--- a/src/Lean/DocString.lean
+++ b/src/Lean/DocString.lean
@@ -4,58 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.DeclarationRange
-import Lean.MonadEnv
-import Init.Data.String.Extra
+import Lean.DocString.Extension
+import Lean.Parser.Tactic.Doc
+
+set_option linter.missingDocs true
+
+-- This module contains the main query interface for docstrings, which assembles user-visible
+-- docstrings.
+-- The module `Lean.DocString.Extension` contains the underlying data.
 
 namespace Lean
+open Lean.Parser.Tactic.Doc
 
-private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
-private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
+/--
+Finds the docstring for a name, taking tactic alternate forms and documentation extensions into
+account.
 
-def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
-  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
-
-def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
-  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
-  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
-
-def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
-  match docString? with
-  | some docString => addDocString declName docString
-  | none => return ()
-
-def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
-  if let some docStr := docStringExt.find? env declName then
-    return some docStr
-  else if includeBuiltin then
-    return (← builtinDocStrings.get).find? declName
-  else
-    return none
-
-structure ModuleDoc where
-  doc : String
-  declarationRange : DeclarationRange
-
-private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
-  addImportedFn := fun _ => {}
-  addEntryFn    := fun s e => s.push e
-  toArrayFn     := fun es => es.toArray
-}
-
-def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
-  moduleDocExt.addEntry env doc
-
-def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
-  moduleDocExt.getState env
-
-def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
-  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
-
-def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
-  match stx.raw[1] with
-  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
-  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
-
-end Lean
+Use `Lean.findSimpleDocString?` to look up the raw docstring without resolving alternate forms or
+including extensions.
+-/
+def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
+  let declName := alternativeOfTactic env declName |>.getD declName
+  let exts := getTacticExtensionString env declName
+  return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts)
diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean
new file mode 100644
index 0000000000..5d16b93051
--- /dev/null
+++ b/src/Lean/DocString/Extension.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.DeclarationRange
+import Lean.MonadEnv
+import Init.Data.String.Extra
+
+-- This module contains the underlying data for docstrings, with as few imports as possible, so that
+-- docstrings can be saved in as much of the compiler as possible.
+-- The module `Lean.DocString` contains the query interface, which needs to look at additional data
+-- to construct user-visible docstrings.
+
+namespace Lean
+
+private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
+private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
+
+def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
+  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
+
+def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
+
+def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+  match docString? with
+  | some docString => addDocString declName docString
+  | none => return ()
+
+/--
+Finds a docstring without performing any alias resolution or enrichment with extra metadata.
+
+Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
+-/
+def findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
+  if let some docStr := docStringExt.find? env declName then
+    return some docStr
+  else if includeBuiltin then
+    return (← builtinDocStrings.get).find? declName
+  else
+    return none
+
+structure ModuleDoc where
+  doc : String
+  declarationRange : DeclarationRange
+
+private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
+  addImportedFn := fun _ => {}
+  addEntryFn    := fun s e => s.push e
+  toArrayFn     := fun es => es.toArray
+}
+
+def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
+  moduleDocExt.addEntry env doc
+
+def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
+  moduleDocExt.getState env
+
+def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
+  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
+
+def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
+  match stx.raw[1] with
+  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
+  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index b1db3658f2..af439ac78e 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -50,3 +50,4 @@ import Lean.Elab.ParseImportsFast
 import Lean.Elab.GuardMsgs
 import Lean.Elab.CheckTactic
 import Lean.Elab.MatchExpr
+import Lean.Elab.Tactic.Doc
diff --git a/src/Lean/Elab/InheritDoc.lean b/src/Lean/Elab/InheritDoc.lean
index 0897ffc7ca..377f9f5952 100644
--- a/src/Lean/Elab/InheritDoc.lean
+++ b/src/Lean/Elab/InheritDoc.lean
@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Elab.InfoTree.Main
-import Lean.DocString
+import Lean.DocString.Extension
 
 namespace Lean
 
@@ -21,9 +21,9 @@ builtin_initialize
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
         let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
-        if (← findDocString? (← getEnv) decl).isSome then
+        if (← findSimpleDocString? (← getEnv) decl).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
-        let some doc ← findDocString? (← getEnv) declName
+        let some doc ← findSimpleDocString? (← getEnv) declName
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
         addDocString decl doc
       | _  => throwError "invalid `[inherit_doc]` attribute"
diff --git a/src/Lean/Elab/Tactic/Doc.lean b/src/Lean/Elab/Tactic/Doc.lean
new file mode 100644
index 0000000000..011fabf512
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Doc.lean
@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+prelude
+import Lean.DocString
+import Lean.Elab.Command
+import Lean.Parser.Tactic.Doc
+import Lean.Parser.Command
+
+namespace Lean.Elab.Tactic.Doc
+open Lean.Parser.Tactic.Doc
+open Lean.Elab.Command
+open Lean.Parser.Command
+
+@[builtin_command_elab «tactic_extension»] def elabTacticExtension : CommandElab
+  | `(«tactic_extension»|tactic_extension%$cmd $_) => do
+    throwErrorAt cmd "Missing documentation comment"
+  | `(«tactic_extension»|$docs:docComment tactic_extension $tac:ident) => do
+    let tacName ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo tac
+
+    if let some tgt' := alternativeOfTactic (← getEnv) tacName then
+        throwErrorAt tac "'{tacName}' is an alternative form of '{tgt'}'"
+    if !(isTactic (← getEnv) tacName) then
+      throwErrorAt tac "'{tacName}' is not a tactic"
+
+    modifyEnv (tacticDocExtExt.addEntry · (tacName, docs.getDocString))
+    pure ()
+  | _ => throwError "Malformed tactic extension command"
+
+@[builtin_command_elab «register_tactic_tag»] def elabRegisterTacticTag : CommandElab
+  | `(«register_tactic_tag»|$[$doc:docComment]? register_tactic_tag $tag:ident $user:str) => do
+    let docstring ← doc.mapM getDocStringText
+    modifyEnv (knownTacticTagExt.addEntry · (tag.getId, user.getString, docstring))
+  | _ => throwError "Malformed 'register_tactic_tag' command"
+
+/--
+Gets the first string token in a parser description. For example, for a declaration like
+`syntax "squish " term " with " term : tactic`, it returns `some "squish "`, and for a declaration
+like `syntax tactic " <;;;> " tactic : tactic`, it returns `some " <;;;> "`.
+
+Returns `none` for syntax declarations that don't contain a string constant.
+-/
+private partial def getFirstTk (e : Expr) : MetaM (Option String) := do
+  match (← Meta.whnf e).getAppFnArgs with
+  | (``ParserDescr.node, #[_, _, p]) => getFirstTk p
+  | (``ParserDescr.trailingNode, #[_, _, _, p]) => getFirstTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getFirstTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getFirstTk p
+  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getFirstTk p
+  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
+  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (some tk)
+  | (``Parser.withAntiquot, #[_, p]) => getFirstTk p
+  | (``Parser.leadingNode, #[_, _, p]) => getFirstTk p
+  | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) =>
+    if let some tk ← getFirstTk p1 then pure (some tk)
+    else getFirstTk (.app p2 (.const ``Unit.unit []))
+  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
+  | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (some tk)
+  | _ => pure none
+
+
+/--
+Creates some `MessageData` for a parser name.
+
+If the parser name maps to a description with an
+identifiable leading token, then that token is shown. Otherwise, the underlying name is shown
+without an `@`. The name includes metadata that makes infoview hovers and the like work. This
+only works for global constants, as the local context is not included.
+-/
+private def showParserName (n : Name) : MetaM MessageData := do
+  let env ← getEnv
+  let params :=
+    env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
+  let tok ←
+    if let some descr := env.find? n |>.bind (·.value?) then
+      if let some tk ← getFirstTk descr then
+        pure <| Std.Format.text tk.trim
+      else pure <| format n
+    else pure <| format n
+  pure <| .ofFormatWithInfos {
+    fmt := "'" ++ .tag 0 tok ++ "'",
+    infos :=
+      .fromList [(0, .ofTermInfo {
+        lctx := .empty,
+        expr := .const n params,
+        stx := .ident .none (toString n).toSubstring n [.decl n []],
+        elaborator := `Delab,
+        expectedType? := none
+      })] _
+  }
+
+
+/--
+Displays all available tactic tags, with documentation.
+-/
+@[builtin_command_elab printTacTags] def elabPrintTacTags : CommandElab := fun _stx => do
+  let all :=
+    tacticTagExt.toEnvExtension.getState (← getEnv)
+      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
+  let mut mapping : NameMap NameSet := {}
+  for arr in all do
+    for (tac, tag) in arr do
+      mapping := mapping.insert tag (mapping.findD tag {} |>.insert tac)
+
+  let showDocs : Option String → MessageData
+    | none => .nil
+    | some d => Format.line ++ MessageData.joinSep ((d.splitOn "\n").map toMessageData) Format.line
+
+  let showTactics (tag : Name) : MetaM MessageData := do
+    match mapping.find? tag with
+    | none => pure .nil
+    | some tacs =>
+      if tacs.isEmpty then pure .nil
+      else
+        let tacs := tacs.toArray.qsort (·.toString < ·.toString) |>.toList
+        pure (Format.line ++ MessageData.joinSep (← tacs.mapM showParserName) ", ")
+
+  let tagDescrs ← liftTermElabM <| (← allTagsWithInfo).mapM fun (name, userName, docs) => do
+    pure <| m!"• " ++
+      MessageData.nestD (m!"'{name}'" ++
+        (if name.toString != userName then m!" — \"{userName}\"" else MessageData.nil) ++
+        showDocs docs ++
+        (← showTactics name))
+
+  let tagList : MessageData :=
+    m!"Available tags: {MessageData.nestD (Format.line ++ .joinSep tagDescrs Format.line)}"
+
+  logInfo tagList
+
+/--
+The information needed to display all documentation for a tactic.
+-/
+structure TacticDoc where
+  /-- The name of the canonical parser for the tactic -/
+  internalName : Name
+  /-- The user-facing name to display (typically the first keyword token) -/
+  userName : String
+  /-- The tags that have been applied to the tactic -/
+  tags : NameSet
+  /-- The docstring for the tactic -/
+  docString : Option String
+  /-- Any docstring extensions that have been specified -/
+  extensionDocs : Array String
+
+def allTacticDocs : MetaM (Array TacticDoc) := do
+  let env ← getEnv
+  let all :=
+    tacticTagExt.toEnvExtension.getState (← getEnv)
+      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
+  let mut tacTags : NameMap NameSet := {}
+  for arr in all do
+    for (tac, tag) in arr do
+      tacTags := tacTags.insert tac (tacTags.findD tac {} |>.insert tag)
+
+  let mut docs := #[]
+
+  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
+    | return #[]
+  for (tac, _) in tactics.kinds do
+    -- Skip noncanonical tactics
+    if let some _ := alternativeOfTactic env tac then continue
+    let userName : String ←
+      if let some descr := env.find? tac |>.bind (·.value?) then
+        if let some tk ← getFirstTk descr then
+          pure tk.trim
+        else pure tac.toString
+      else pure tac.toString
+
+    docs := docs.push {
+      internalName := tac,
+      userName := userName,
+      tags := tacTags.findD tac {},
+      docString := ← findDocString? env tac,
+      extensionDocs := getTacticExtensions env tac
+    }
+  return docs
diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean
index c68bca90fd..bd21b4ad10 100644
--- a/src/Lean/Parser.lean
+++ b/src/Lean/Parser.lean
@@ -12,6 +12,7 @@ import Lean.Parser.Command
 import Lean.Parser.Module
 import Lean.Parser.Syntax
 import Lean.Parser.Do
+import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser
diff --git a/src/Lean/Parser/Attr.lean b/src/Lean/Parser/Attr.lean
index 1c19f4c85b..27473f7b96 100644
--- a/src/Lean/Parser/Attr.lean
+++ b/src/Lean/Parser/Attr.lean
@@ -50,6 +50,24 @@ def externEntry := leading_parser
 @[builtin_attr_parser] def extern     := leading_parser
   nonReservedSymbol "extern" >> optional (ppSpace >> numLit) >> many (ppSpace >> externEntry)
 
+/--
+Declare this tactic to be an alias or alternative form of an existing tactic.
+
+This has the following effects:
+ * The alias relationship is saved
+ * The docstring is taken from the original tactic, if present
+-/
+@[builtin_attr_parser] def «tactic_alt» := leading_parser
+  "tactic_alt" >> ppSpace >> ident
+
+/--
+Add one or more tags to a tactic.
+
+Tags should be applied to the canonical names for tactics.
+-/
+@[builtin_attr_parser] def «tactic_tag» := leading_parser
+  "tactic_tag" >> many1 (ppSpace >> ident)
+
 end Attr
 
 end Lean.Parser
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index f94a85ba23..15a0beb37e 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -447,6 +447,11 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
   "#print " >> nonReservedSymbol "axioms " >> ident
 @[builtin_command_parser] def printEqns      := leading_parser
   "#print " >> (nonReservedSymbol "equations " <|> nonReservedSymbol "eqns ") >> ident
+/--
+Displays all available tactic tags, with documentation.
+-/
+@[builtin_command_parser] def printTacTags   := leading_parser
+  "#print " >> nonReservedSymbol "tactic " >> nonReservedSymbol "tags"
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
@@ -669,6 +674,26 @@ Documentation can only be added to declarations in the same module.
 @[builtin_command_parser] def addDocString := leading_parser
   docComment >> "add_decl_doc " >> ident
 
+/--
+Register a tactic tag, saving its user-facing name and docstring.
+
+Tactic tags can be used by documentation generation tools to classify related tactics.
+-/
+@[builtin_command_parser] def «register_tactic_tag» := leading_parser
+  optional (docComment >> ppLine) >>
+  "register_tactic_tag " >> ident >> strLit
+
+/--
+Add more documentation as an extension of the documentation for a given tactic.
+
+The extended documentation is placed in the command's docstring. It is shown as part of a bulleted
+list, so it should be brief.
+-/
+@[builtin_command_parser] def «tactic_extension» := leading_parser
+  optional (docComment >> ppLine) >>
+  "tactic_extension " >> ident
+
+
 /--
   This is an auxiliary command for generation constructor injectivity theorems for
   inductive types defined at `Prelude.lean`.
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 7b32c45790..58c674a146 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Term
+import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser
diff --git a/src/Lean/Parser/Tactic/Doc.lean b/src/Lean/Parser/Tactic/Doc.lean
new file mode 100644
index 0000000000..8b4d25cd07
--- /dev/null
+++ b/src/Lean/Parser/Tactic/Doc.lean
@@ -0,0 +1,290 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+prelude
+import Lean.Attributes
+import Lean.DocString.Extension
+import Lean.Elab.InfoTree.Main
+import Lean.Parser.Attr
+import Lean.Parser.Extension
+
+set_option linter.missingDocs true
+
+namespace Lean.Parser.Tactic.Doc
+
+open Lean.Parser (registerParserAttributeHook)
+open Lean.Parser.Attr
+
+/-- Check whether a name is a tactic syntax kind -/
+def isTactic (env : Environment) (kind : Name) : Bool := Id.run do
+  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
+    | return false
+  for (tac, _) in tactics.kinds do
+    if kind == tac then return true
+  return false
+
+/--
+Stores a collection of *tactic alternatives*, to track which new syntax rules represent new forms of
+existing tactics.
+-/
+builtin_initialize tacticAlternativeExt
+    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap Name) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun as (src, tgt) => as.insert src tgt,
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/--
+If `tac` is registered as the alternative form of another tactic, then return the canonical name for
+it.
+-/
+def alternativeOfTactic (env : Environment) (tac : Name) : Option Name :=
+  match env.getModuleIdxFor? tac with
+  | some modIdx =>
+    match (tacticAlternativeExt.getModuleEntries env modIdx).binSearch (tac, .anonymous) (Name.quickLt ·.1 ·.1) with
+    | some (_, val) => some val
+    | none => none
+  | none => tacticAlternativeExt.getState env |>.find? tac
+
+/--
+Find all alternatives for a given canonical tactic name.
+-/
+def aliases [Monad m] [MonadEnv m] (tac : Name) : m NameSet := do
+  let env ← getEnv
+  let mut found := {}
+  for (src, tgt) in tacticAlternativeExt.getState env do
+    if tgt == tac then found := found.insert src
+  for arr in tacticAlternativeExt.toEnvExtension.getState env |>.importedEntries do
+    for (src, tgt) in arr do
+      if tgt == tac then found := found.insert src
+  pure found
+
+builtin_initialize
+  let name := `tactic_alt
+  registerBuiltinAttribute {
+    name := name,
+    ref := by exact decl_name%,
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
+      unless ((← getEnv).getModuleIdxFor? decl).isNone do
+        throwError "invalid attribute '{name}', declaration is in an imported module"
+      let `(«tactic_alt»|tactic_alt $tgt) := stx
+        | throwError "invalid syntax for '{name}' attribute"
+
+      let tgtName ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo tgt
+
+      if !(isTactic (← getEnv) tgtName) then throwErrorAt tgt "'{tgtName}' is not a tactic"
+      -- If this condition is true, then we're in an `attribute` command and can validate here.
+      if (← getEnv).find? decl |>.isSome then
+        if !(isTactic (← getEnv) decl) then throwError "'{decl}' is not a tactic"
+
+      if let some tgt' := alternativeOfTactic (← getEnv) tgtName then
+        throwError "'{tgtName}' is itself an alternative for '{tgt'}'"
+      modifyEnv fun env => tacticAlternativeExt.addEntry env (decl, tgtName)
+      if (← findSimpleDocString? (← getEnv) decl).isSome then
+        logWarningAt stx m!"Docstring for '{decl}' will be ignored because it is an alternative"
+
+    descr :=
+      "Register a tactic parser as an alternative form of an existing tactic, so they " ++
+      "can be grouped together in documentation.",
+    -- This runs prior to elaboration because it allows a check for whether the decl is present
+    -- in the environment to determine whether we can see if it's a tactic name. This is useful
+    -- when the attribute is applied after definition, using an `attribute` command (error checking
+    -- for the `@[tactic_alt TAC]` syntax is performed by the parser attribute hook). If this
+    -- attribute ran later, then the decl would already be present.
+    applicationTime := .beforeElaboration
+  }
+
+
+/--
+The known tactic tags that allow tactics to be grouped by purpose.
+-/
+builtin_initialize knownTacticTagExt
+    : PersistentEnvExtension
+        (Name × String × Option String)
+        (Name × String × Option String)
+        (NameMap (String × Option String)) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun as (src, tgt) => as.insert src tgt,
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/--
+Get the user-facing name and docstring for a tactic tag.
+-/
+def tagInfo [Monad m] [MonadEnv m] (tag : Name) : m (Option (String × Option String)) := do
+  let env ← getEnv
+  match env.getModuleIdxFor? tag with
+  | some modIdx =>
+    match (knownTacticTagExt.getModuleEntries env modIdx).binSearch (tag, default) (Name.quickLt ·.1 ·.1) with
+    | some (_, val) => pure (some val)
+    | none => pure none
+  | none => pure (knownTacticTagExt.getState env |>.find? tag)
+
+/-- Enumerate the tactic tags that are available -/
+def allTags [Monad m] [MonadEnv m] : m (List Name) := do
+  let env ← getEnv
+  let mut found : NameSet := {}
+  for (tag, _) in knownTacticTagExt.getState env do
+    found := found.insert tag
+  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
+    for (tag, _) in arr do
+      found := found.insert tag
+  pure (found.toArray.qsort (·.toString < ·.toString) |>.toList)
+
+/-- Enumerate the tactic tags that are available, with their user-facing name and docstring -/
+def allTagsWithInfo [Monad m] [MonadEnv m] : m (List (Name × String × Option String)) := do
+  let env ← getEnv
+  let mut found : NameMap (String × Option String) := {}
+  for (tag, info) in knownTacticTagExt.getState env do
+    found := found.insert tag info
+  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
+    for (tag, info) in arr do
+      found := found.insert tag info
+  let arr := found.fold (init := #[]) (fun arr k v => arr.push (k, v))
+  pure (arr.qsort (·.1.toString < ·.1.toString) |>.toList)
+
+/--
+The mapping between tags and tactics. Tags may be applied in any module, not just the defining
+module for the tactic.
+
+Because this is expected to be augmented regularly, but queried rarely (only when generating
+documentation indices), it is just stored as flat unsorted arrays of pairs. Before it is used for
+some other purpose, consider a new representation.
+
+The first projection in each pair is the tactic name, and the second is the tag name.
+-/
+builtin_initialize tacticTagExt
+    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap NameSet) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun tags (decl, newTag) => tags.insert decl (tags.findD decl {} |>.insert newTag)
+    exportEntriesFn := fun tags => Id.run do
+      let mut exported := #[]
+      for (decl, dTags) in tags do
+        for t in dTags do
+          exported := exported.push (decl, t)
+      exported
+  }
+
+builtin_initialize
+  let name := `tactic_tag
+  registerBuiltinAttribute {
+    name := name,
+    ref := by exact decl_name%,
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
+      let `(«tactic_tag»|tactic_tag $tags*) := stx
+        | throwError "invalid '{name}' attribute"
+      if (← getEnv).find? decl |>.isSome then
+        if !(isTactic (← getEnv) decl) then
+          throwErrorAt stx "'{decl}' is not a tactic"
+
+      if let some tgt' := alternativeOfTactic (← getEnv) decl then
+        throwErrorAt stx "'{decl}' is an alternative form of '{tgt'}'"
+
+      for t in tags do
+        let tagName := t.getId
+        if let some _ ← tagInfo tagName then
+          modifyEnv (tacticTagExt.addEntry · (decl, tagName))
+        else
+          let all ← allTags
+          let extra : MessageData :=
+              let count := all.length
+              let name := (m!"'{·}'")
+              let suggestions :=
+                if count == 0 then m!"(no tags defined)"
+                else if count == 1 then
+                  MessageData.joinSep (all.map name) ", "
+                else if count < 10 then
+                  m!"one of " ++ MessageData.joinSep (all.map name) ", "
+                else
+                  m!"one of " ++
+                  MessageData.joinSep (all.take 10 |>.map name) ", " ++ ", ..."
+              m!"(expected {suggestions})"
+
+          throwErrorAt t (m!"unknown tag '{tagName}' " ++ extra)
+    descr := "Register a tactic parser as an alternative of an existing tactic, so they can be " ++
+      "grouped together in documentation.",
+    -- This runs prior to elaboration because it allows a check for whether the decl is present
+    -- in the environment to determine whether we can see if it's a tactic name. This is useful
+    -- when the attribute is applied after definition, using an `attribute` command (error checking
+    -- for the `@[tactic_tag ...]` syntax is performed by the parser attribute hook). If this
+    -- attribute ran later, then the decl would already be present.
+    applicationTime := .beforeElaboration
+  }
+
+/--
+Extensions to tactic documentation.
+
+This provides a structured way to indicate that an extensible tactic has been extended (for
+instance, new cases tried by `trivial`).
+-/
+builtin_initialize tacticDocExtExt
+    : PersistentEnvExtension (Name × Array String) (Name × String) (NameMap (Array String)) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun es (x, ext) => es.insert x (es.findD x #[] |>.push ext),
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/-- Gets the extensions declared for the documentation for the given canonical tactic name -/
+def getTacticExtensions (env : Environment) (tactic : Name) : Array String := Id.run do
+  let mut extensions := #[]
+  -- Extensions may be declared in any module, so they must all be searched
+  for modArr in tacticDocExtExt.toEnvExtension.getState env |>.importedEntries do
+    if let some (_, strs) := modArr.binSearch (tactic, #[]) (Name.quickLt ·.1 ·.1) then
+      extensions := extensions ++ strs
+  if let some strs := tacticDocExtExt.getState env |>.find? tactic then
+    extensions := extensions ++ strs
+  pure extensions
+
+/-- Gets the rendered extensions for the given canonical tactic name -/
+def getTacticExtensionString (env : Environment) (tactic : Name) : String := Id.run do
+  let exts := getTacticExtensions env tactic
+  if exts.size == 0 then ""
+  else "\n\nExtensions:\n\n" ++ String.join (exts.toList.map bullet) |>.trimRight
+where
+  indentLine (str: String) : String :=
+    (if str.all (·.isWhitespace) then str else "   " ++ str) ++ "\n"
+  bullet (str : String) : String :=
+    let lines := str.splitOn "\n"
+    match lines with
+    | [] => ""
+    | [l] => " * " ++ l ++ "\n\n"
+    | l::ls => " * " ++ l ++ "\n" ++ String.join (ls.map indentLine) ++ "\n\n"
+
+
+-- Note: this error handler doesn't prevent all cases of non-tactics being added to the data
+-- structure. But the module will throw errors during elaboration, and there doesn't seem to be
+-- another way to implement this, because the category parser extension attribute runs *after* the
+-- attributes specified before a `syntax` command.
+/--
+Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are
+tactics.
+-/
+def tacticDocsOnTactics : ParserAttributeHook where
+  postAdd (catName declName : Name) (_builtIn : Bool) := do
+    if catName == `tactic then
+      return
+    if alternativeOfTactic (← getEnv) declName |>.isSome then
+      throwError m!"'{declName}' is not a tactic"
+    -- It's sufficient to look in the state (and not the imported entries) because this validation
+    -- only needs to check tags added in the current module
+    if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then
+      if !tags.isEmpty then
+        throwError m!"'{declName}' is not a tactic"
+
+builtin_initialize
+  registerParserAttributeHook tacticDocsOnTactics
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index de5a777ff3..5a1dd9590d 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -10,6 +10,8 @@ import Lean.DeclarationRange
 import Lean.Data.Json
 import Lean.Data.Lsp
 
+import Lean.Parser.Tactic.Doc
+
 import Lean.Server.FileWorker.Utils
 import Lean.Server.Requests
 import Lean.Server.Completion
@@ -24,6 +26,8 @@ open Lsp
 open RequestM
 open Snapshots
 
+open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
+
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
   let doc ← readDoc
@@ -85,7 +89,8 @@ def handleHover (p : HoverParams)
       let stxDoc? ← match stack? with
         | some stack => stack.findSomeM? fun (stx, _) => do
           let .node _ kind _ := stx | pure none
-          return (← findDocString? snap.env kind).map (·, stx.getRange?.get!)
+          let docStr ← findDocString? snap.env kind
+          return docStr.map (·, stx.getRange?.get!)
         | none => pure none
 
       -- now try info tree
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 70c51033a3..9e4fc1913c 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -5,10 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 prelude
+import Lean.DocString
 import Lean.PrettyPrinter
+import Lean.Parser.Tactic.Doc
 
 namespace Lean.Elab
 
+open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
+
 /-- Elaborator information with elaborator context.
 
 It can be thought of as a "thunked" elaboration computation that allows us
@@ -244,7 +248,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   match i with
   | .ofTermInfo ti =>
     if let some n := ti.expr.constName? then
-      return ← findDocString? env n
+      return (← findDocString? env n)
   | .ofFieldInfo fi => return ← findDocString? env fi.projName
   | .ofOptionInfo oi =>
     if let some doc ← findDocString? env oi.declName then
@@ -258,6 +262,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
   return none
 
+
 /-- Construct a hover popup, if any, from an info node in a context.-/
 def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
   ci.runMetaM i.lctx do
diff --git a/src/lake/Lake/Load/Lean/Eval.lean b/src/lake/Lake/Load/Lean/Eval.lean
index 2b3f6cc1ed..67ed546e41 100644
--- a/src/lake/Lake/Load/Lean/Eval.lean
+++ b/src/lake/Lake/Load/Lean/Eval.lean
@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.DSL.Attributes
 import Lake.Config.Workspace
+import Lean.DocString
 
 /-! # Lean Configuration Evaluator
 
diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h
index 0699845ba4..658ab0874e 100644
--- a/src/stdlib_flags.h
+++ b/src/stdlib_flags.h
@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);
diff --git a/tests/lean/interactive/hoverTacticExt.lean b/tests/lean/interactive/hoverTacticExt.lean
new file mode 100644
index 0000000000..e88154d6ff
--- /dev/null
+++ b/tests/lean/interactive/hoverTacticExt.lean
@@ -0,0 +1,61 @@
+
+
+
+/-!
+Tests that docstring hovers are computed correctly for tactic extensions
+-/
+
+/-- Another `trivial` tactic -/
+syntax (name := my_trivial) "my_trivial" : tactic
+
+@[tactic_alt my_trivial]
+syntax (name := very_trivial) "very_trivial" : tactic
+macro_rules
+| `(tactic|very_trivial) => `(tactic|my_trivial)
+
+/-- It tries Lean's `trivial` -/
+tactic_extension my_trivial
+               --^ textDocument/hover
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|trivial)
+             --^ textDocument/hover
+
+/-- It tries `simp_all` -/
+tactic_extension my_trivial
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|simp_all; done)
+
+
+example : True := by
+  my_trivial
+      --^ textDocument/hover
+
+/-- It tries `constructor` -/
+tactic_extension my_trivial
+               --^ textDocument/hover
+-- On the preceding line, it was not yet extended.
+-- Here, it is:
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|constructor; done)
+           --^ textDocument/hover
+
+/--
+It tries some useful things:
+ * `omega`
+ * `simp_arith [*]`
+-/
+tactic_extension my_trivial
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|omega)
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|simp_arith [*]; done)
+
+-- This tests that nested lists work
+example : True := by
+  my_trivial
+      --^ textDocument/hover
+
+-- This tests that alts are resolved
+example : True := by
+  very_trivial
+      --^ textDocument/hover
diff --git a/tests/lean/interactive/hoverTacticExt.lean.expected.out b/tests/lean/interactive/hoverTacticExt.lean.expected.out
new file mode 100644
index 0000000000..243567103a
--- /dev/null
+++ b/tests/lean/interactive/hoverTacticExt.lean.expected.out
@@ -0,0 +1,56 @@
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 16, "character": 17}}
+{"range":
+ {"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 27}},
+ "contents":
+ {"value":
+  "```lean\nmy_trivial : Lean.ParserDescr\n```\n***\nAnother `trivial` tactic ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 19, "character": 15}}
+{"range":
+ {"start": {"line": 19, "character": 13}, "end": {"line": 19, "character": 23}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 29, "character": 8}}
+{"range":
+ {"start": {"line": 29, "character": 2}, "end": {"line": 29, "character": 12}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 33, "character": 17}}
+{"range":
+ {"start": {"line": 33, "character": 17}, "end": {"line": 33, "character": 27}},
+ "contents":
+ {"value":
+  "```lean\nmy_trivial : Lean.ParserDescr\n```\n***\nAnother `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 38, "character": 13}}
+{"range":
+ {"start": {"line": 38, "character": 13}, "end": {"line": 38, "character": 23}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all` \n\n * It tries `constructor`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 54, "character": 8}}
+{"range":
+ {"start": {"line": 54, "character": 2}, "end": {"line": 54, "character": 12}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all` \n\n * It tries `constructor` \n\n * It tries some useful things:\n    * `omega`\n    * `simp_arith [*]`",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverTacticExt.lean"},
+ "position": {"line": 59, "character": 8}}
+{"range":
+ {"start": {"line": 59, "character": 2}, "end": {"line": 59, "character": 14}},
+ "contents":
+ {"value":
+  "Another `trivial` tactic \n\nExtensions:\n\n * It tries Lean's `trivial` \n\n * It tries `simp_all` \n\n * It tries `constructor` \n\n * It tries some useful things:\n    * `omega`\n    * `simp_arith [*]`",
+  "kind": "markdown"}}
diff --git a/tests/lean/run/tacticDoc.lean b/tests/lean/run/tacticDoc.lean
new file mode 100644
index 0000000000..ae782a86b9
--- /dev/null
+++ b/tests/lean/run/tacticDoc.lean
@@ -0,0 +1,136 @@
+/-!
+Test the commands and attributes for interacting with tactic documentation.
+
+Note that when the standard library starts shipping with actual tags, then this test will need to be
+adjusted or rewritten, as it depends on the complete set of tags that are transitively accessible.
+We don't expect to modify the default tactics often, and it should be a matter of accepting changes
+from #guard_msgs.
+-/
+
+set_option guard_msgs.diff true
+
+/-- Finishing tactics that are intended to completely close a goal -/
+register_tactic_tag finishing "finishing"
+
+/-- Tactics that are intended to be extensible -/
+register_tactic_tag extensible "extensible"
+
+/-- Tactics that sequence or arrange other tactics -/
+register_tactic_tag ctrl "control flow"
+
+/-- Another `trivial` tactic -/
+@[tactic_tag finishing extensible]
+syntax (name := my_trivial) "my_trivial" : tactic
+
+@[tactic_alt my_trivial]
+syntax (name := very_trivial) "very_trivial" : tactic
+
+/-- It tries Lean's `trivial` -/
+tactic_extension my_trivial
+
+macro_rules
+  | `(tactic|my_trivial) => `(tactic|trivial)
+
+attribute [tactic_tag finishing] Lean.Parser.Tactic.omega
+
+attribute [tactic_tag ctrl] Lean.Parser.Tactic.«tactic_<;>_»
+
+/-!
+# Error Handling
+
+Test error handling. Non-tactics are not eligible to be the target of alternatives, to be
+alternatives themselves, or to receive tags or doc extensions.
+-/
+
+/-! These tests check that non-tactics can't be alternative forms of tactics -/
+
+/-- error: 'nonTacticTm' is not a tactic -/
+#guard_msgs in
+@[tactic_alt my_trivial]
+syntax (name := nonTacticTm) "nonTactic" : term
+
+syntax (name := nonTacticTm') "nonTactic'" : term
+
+/-- error: 'nonTacticTm'' is not a tactic -/
+#guard_msgs in
+attribute [tactic_alt my_trivial] nonTacticTm'
+
+/-! These tests check that non-tactics can't have tactic alternatives -/
+
+/-- error: 'nonTacticTm' is not a tactic -/
+#guard_msgs in
+@[tactic_alt nonTacticTm]
+syntax (name := itsATactic) "yepATactic" : tactic
+
+syntax (name := itsATactic') "yepATactic'" : tactic
+
+/-- error: 'nonTacticTm' is not a tactic -/
+#guard_msgs in
+attribute [tactic_alt nonTacticTm] itsATactic'
+
+
+/-! These tests check that non-tactics can't receive tags -/
+
+/-- error: 'tm' is not a tactic -/
+#guard_msgs in
+@[tactic_tag finishing]
+syntax (name := tm) "someTerm" : term
+
+
+/-- error: 'tm' is not a tactic -/
+#guard_msgs in
+attribute [tactic_tag ctrl] tm
+
+/-! These tests check that only known tags may be applied -/
+
+/-- error: unknown tag 'bogus' (expected one of 'ctrl', 'extensible', 'finishing') -/
+#guard_msgs in
+attribute [tactic_tag bogus] my_trivial
+
+/-- error: unknown tag 'bogus' (expected one of 'ctrl', 'extensible', 'finishing') -/
+#guard_msgs in
+@[tactic_tag bogus]
+syntax "someTactic" : tactic
+
+/-! Check that only canonical tactics may receive doc extensions -/
+
+/-- error: 'nonTacticTm'' is not a tactic -/
+#guard_msgs in
+/-- Some docs that don't belong here -/
+tactic_extension nonTacticTm'
+
+/-- error: 'very_trivial' is an alternative form of 'my_trivial' -/
+#guard_msgs in
+/-- Some docs that don't belong here -/
+tactic_extension very_trivial
+
+/-! Check that warnings are issued if alternatives have their own docstrings -/
+
+/-- warning: Docstring for 'tacticAnother' will be ignored because it is an alternative -/
+#guard_msgs in
+/-- Docs -/
+@[tactic_alt my_trivial]
+syntax "another" : tactic
+
+/-- Docs -/
+syntax (name := yetAnother) "yetAnother" : tactic
+
+/-- warning: Docstring for 'yetAnother' will be ignored because it is an alternative -/
+#guard_msgs in
+attribute [tactic_alt my_trivial] «yetAnother»
+
+/-! # Querying Tactic Docs -/
+/--
+info: Available tags: ⏎
+  • 'ctrl' — "control flow"
+    Tactics that sequence or arrange other tactics ⏎
+    '<;>'
+  • 'extensible'
+    Tactics that are intended to be extensible ⏎
+    'my_trivial'
+  • 'finishing'
+    Finishing tactics that are intended to completely close a goal ⏎
+    'omega', 'my_trivial', 'someTerm'
+-/
+#guard_msgs in
+#print tactic tags