diff options
| -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. |