aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Ambroise <chaster_killer@hotmail.fr>2018-06-28 14:04:12 +0200
committerGravatar GitHub <noreply@github.com>2018-06-28 14:04:12 +0200
commitf00843701373257c069d33e84b78ecaeae9e4cb0 (patch)
treead2fbfc6531fc58794927cf10b9fca732666a4e8 /doc
parent2636bf4cf12519ef1c0bf3a3a2fb2eb9194bf278 (diff)
Update gallina-extensions.rst
I knew this feature existed but I did not remember the syntax and I could not find it in the manual
Diffstat (limited to 'doc')
-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 294ac5799..954e10340 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 ``?``\ [`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`).