diff options
| author | Pierre-Marie Pédrot | 2021-01-21 16:54:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-10 12:23:41 +0100 |
| commit | 234a802f0925f9c9078417afa28dcb00c31668d9 (patch) | |
| tree | f9067fd5fb8a4bc0dd51361999377a1895b51662 /doc/sphinx/using | |
| parent | e976e2cc4ad8fd361aa54b071543f75dbb532ccd (diff) | |
Add documentation.
Diffstat (limited to 'doc/sphinx/using')
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 917edf0774..7461bfe443 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -22,13 +22,17 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)` by a comma. This attribute is supported by the following commands: :cmd:`Ltac`, - :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. + :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`, :cmd:`Ltac2`, + :cmd:`Ltac2 Notation`, :cmd:`Ltac2 external`. It can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string__since. @string__note. Tactic Notation @qualid is deprecated since @string__since. @string__note. Notation @string is deprecated since @string__since. @string__note. + Ltac2 definition @qualid is deprecated since @string__since. @string__note. + Ltac2 alias @qualid is deprecated since @string__since. @string__note. + Ltac2 notation {+ @ltac2_scope } is deprecated since @string__since. @string__note. :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number, :n:`@string__note` is |