diff options
| author | Jim Fehrle | 2020-09-06 19:09:05 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-11-09 15:59:54 -0800 |
| commit | a9658f29280dd7c00f5b50942da5f8225f28c754 (patch) | |
| tree | 059831be2adcc8485e535fbac465ab3667e5b237 /doc/sphinx/proof-engine | |
| parent | e38d3bac150b709ffbbe6115723ce97177ace638 (diff) | |
Add global version of OPTINREF
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b912bcbdf8..81c497d60a 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1633,7 +1633,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. insertprodn ltac2_oriented_rewriter ltac2_rewriter .. prodn:: - ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter + ltac2_oriented_rewriter ::= {? {| -> | <- } } @ltac2_rewriter ltac2_rewriter ::= {? @natural } {? {| ? | ! } } @ltac2_constr_with_bindings .. insertprodn ltac2_for_each_goal ltac2_goal_tactics |