From 1eb1fe7cee6f8381c5c715430eba0c5994f0b3a4 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 13 Mar 2019 09:54:28 +0100
Subject: [refman] Fix Sphinx-translation regression in Arguments command.

---
 doc/sphinx/language/gallina-extensions.rst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index c87d197179..59506a6ff2 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1575,7 +1575,7 @@ Declaring Implicit Arguments
 
 
 
-.. cmd:: Arguments @qualid {* [ @ident ] | @ident }
+.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident }
    :name: Arguments (implicits)
 
    This command is used to set implicit arguments *a posteriori*,
@@ -1592,20 +1592,20 @@ Declaring Implicit Arguments
 
    This command clears implicit arguments.
 
-.. cmdv:: Global Arguments @qualid {* [ @ident ] | @ident }
+.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident }
 
    This command is used to recompute the implicit arguments of
    :token:`qualid` after ending of the current section if any, enforcing the
    implicit arguments known from inside the section to be the ones
    declared by the command.
 
-.. cmdv:: Local Arguments @qualid {* [ @ident ] | @ident }
+.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident }
 
    When in a module, tell not to activate the
    implicit arguments of :token:`qualid` declared by this command to contexts that
    require the module.
 
-.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | @ident } }
+.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } }
 
    For names of constants, inductive types,
    constructors, lemmas which can only be applied to a fixed number of
-- 
cgit v1.2.3