diff options
| author | Théo Zimmermann | 2020-11-09 16:28:29 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-09 16:41:57 +0100 |
| commit | c0b48997dc7fccd15ab237df6274dbcfa05cbc9c (patch) | |
| tree | 681ac33f33677e3bd6ba3b893132eb6caa794a1a | |
| parent | d2047c6368ae11a3a3fd7f2db8c991d135094e60 (diff) | |
Fix indentation of todo in Ltac chapter.
Actual documentation was interpreted as a comment.
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 16 |
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. |