Fix indentation of todo in Ltac chapter.

Actual documentation was interpreted as a comment.

1 files changed, 11 insertions, 5 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 8663ac646b..ae3a252570 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1754,10 +1754,15 @@ Defining |Ltac| symbols
       Defines a user-defined symbol, but gives an error if the symbol has already
       been defined.
 
-.. todo apparent inconsistency: "Ltac intros := idtac" seems like it redefines/hides an existing tactic,
-      but in fact it creates a tactic which can only be called by it's qualified name.  This is true in general
-      of tactic notations.  The only way to overwrite most primitive tactics, and any user-defined tactic
-      notation, is with another tactic notation.
+      .. todo apparent inconsistency:
+
+         "Ltac intros := idtac" seems like it redefines/hides an
+         existing tactic, but in fact it creates a tactic which can
+         only be called by its qualified name.  This is true in
+         general of tactic notations.  The only way to overwrite most
+         primitive tactics, and any user-defined tactic notation, is
+         with another tactic notation.
+
       .. exn:: There is already an Ltac named @qualid
          :undocumented:
 
@@ -1767,7 +1772,8 @@ Defining |Ltac| symbols
       do not count as user-defined tactics for `::=`.  If :attr:`local` is not
       specified, the redefinition applies across module boundaries.
 
-      .. exn: There is no Ltac named @qualid
+      .. exn:: There is no Ltac named @qualid
+         :undocumented:
 
    :n:`{* with @tacdef_body }`
       Permits definition of mutually recursive tactics.