From feb9c50b5812a01e9dc60e2408f4f9f38986ce8c Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 10 May 2019 22:29:57 -0400
Subject: [refman] Introduce syntax for alternatives in notations

Closes GH-8482.
---
 doc/sphinx/addendum/program.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/addendum/program.rst')

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index b410833d25..22ddcae584 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved
 obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
-.. cmd:: {? Local|Global} Obligation Tactic := @tactic
+.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic
    :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
-- 
cgit v1.2.3