From a9658f29280dd7c00f5b50942da5f8225f28c754 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 6 Sep 2020 19:09:05 -0700
Subject: Add global version of OPTINREF

---
 doc/sphinx/proof-engine/ltac2.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/proof-engine')

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
-- 
cgit v1.2.3