aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx
diff options
context:
space:
mode:
authorGravatar Ambroise <chaster_killer@hotmail.fr>2018-06-28 14:52:36 +0200
committerGravatar Ambroise <chaster_killer@hotmail.fr>2018-06-28 14:52:36 +0200
commit5b96722d51026c47fe569df85a5ffc4d14397d12 (patch)
tree51557da0345b29b577650a6549255b63102c9eb7 /doc/sphinx
parentf00843701373257c069d33e84b78ecaeae9e4cb0 (diff)
wrong sphinx syntax
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/language/gallina-extensions.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 954e10340..8fbd2ea4e 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2228,7 +2228,7 @@ existential variable used in the same context as its context of definition is wr
Check (fun x y => _) 0 1.
Existential variables can be named by the user upon creation using
-the syntax ``?``\ [`ident`]. This is useful when the existential
+the syntax :n:`?[@ident]`. This is useful when the existential
variable needs to be explicitly handled later in the script (e.g.
with a named-goal selector, see :ref:`goal-selectors`).