diff options
| author | coqbot-app[bot] | 2020-10-25 20:00:32 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-25 20:00:32 +0000 |
| commit | a12112c15cdcb0467d4cf5f5a7cfa639852ccd49 (patch) | |
| tree | 3e2d8983efe06e93cbfab75a65b4f4420525332a /doc/sphinx/user-extensions/syntax-extensions.rst | |
| parent | d397f10bf4d334189523e187b2cd5fd6e18b4bcc (diff) | |
| parent | 7a57a23e4fb8a74e8746d4eaee900f2ced37a28a (diff) | |
Merge PR #12936: Convert misc chapters to prodn, update syntax
Reviewed-by: Zimmi48
Ack-by: mattam82
Ack-by: pi8027
Ack-by: herbelin
Ack-by: gares
Ack-by: fajb
Ack-by: proux01
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 1791c53aa8..0c51361b64 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -385,8 +385,8 @@ a :token:`decl_notations` clause after the definition of the (co)inductive type (co)recursive term (or after the definition of each of them in case of mutual definitions). The exact syntax is given by :n:`@decl_notation` for inductive, co-inductive, recursive and corecursive definitions and in :ref:`record-types` -for records. Note that only syntax modifiers that do not require to add or -change a parsing rule are accepted. +for records. Note that only syntax modifiers that do not require adding or +changing a parsing rule are accepted. .. insertprodn decl_notations decl_notation @@ -1894,12 +1894,12 @@ Tactic notations allow customizing the syntax of tactics. - :tacn:`unfold`, :tacn:`with_strategy` * - ``constr`` - - :token:`term` + - :token:`one_term` - a term - :tacn:`exact` * - ``uconstr`` - - :token:`term` + - :token:`one_term` - an untyped term - :tacn:`refine` |