diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 5c091f04ac..8663ac646b 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -161,7 +161,7 @@ Syntactic values Provides a way to use the syntax and semantics of a grammar nonterminal as a value in an :token:`ltac_expr`. The table below describes the most useful of these. You can see the others by running ":cmd:`Print Grammar` `tactic`" and -examining the part at the end under "Entry tactic:tactic_arg". +examining the part at the end under "Entry tactic:tactic_value". :token:`ident` name of a grammar nonterminal listed in the table diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index fc5aa3f93d..06018304ab 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -444,7 +444,7 @@ Displaying information about notations This command doesn't display all nonterminals of the grammar. For example, productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` - and `tactic_then_gen` which are not shown and can't be printed. + and `for_each_goal` which are not shown and can't be printed. Most of the grammar in the documentation was updated in 8.12 to make it accurate and readable. This was done using a new developer tool that extracts the grammar from the @@ -486,7 +486,7 @@ Displaying information about notations | "4" LEFTA [ SELF; ";"; binder_tactic | SELF; ";"; SELF - | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] + | SELF; ";"; tactic_then_locality; for_each_goal; "]" ] | "3" RIGHTA [ IDENT "try"; SELF : |