From 5b96722d51026c47fe569df85a5ffc4d14397d12 Mon Sep 17 00:00:00 2001 From: Ambroise Date: Thu, 28 Jun 2018 14:52:36 +0200 Subject: wrong sphinx syntax --- doc/sphinx/language/gallina-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') 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`). -- cgit v1.2.3