diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-28 15:29:47 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-28 15:29:47 +0200 |
| commit | 1fab152558a941c500067599d6b2043e1176a446 (patch) | |
| tree | d7466b103c9adeacb05bfbc110688534a0709d01 /doc | |
| parent | aa44f98e8a8586f4bc1b96a69f6f39c1f20bed5e (diff) | |
| parent | 5b96722d51026c47fe569df85a5ffc4d14397d12 (diff) | |
Merge PR #7948: Syntax for naming an existential variable
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..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`). |