diff options
author | Ambroise <chaster_killer@hotmail.fr> | 2018-06-28 14:04:12 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-28 14:04:12 +0200 |
commit | f00843701373257c069d33e84b78ecaeae9e4cb0 (patch) | |
tree | ad2fbfc6531fc58794927cf10b9fca732666a4e8 /doc | |
parent | 2636bf4cf12519ef1c0bf3a3a2fb2eb9194bf278 (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.rst | 2 |
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`). |