diff options
| author | Théo Zimmermann | 2017-06-12 12:27:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-06-13 09:42:34 +0200 |
| commit | 39f36789b986779d36acd36cfa1425487bad43c3 (patch) | |
| tree | b7e32adbbefb7edd29a16225c76edb35ad962bb3 | |
| parent | ce1e1dba837ad6e2c79ff7e531b5e3adea3cd327 (diff) | |
Document evar naming syntax.
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 5 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 |
2 files changed, 6 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index b475a5233c..3f2dd73a39 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1990,6 +1990,11 @@ Check (fun x y => _) 0 1. Unset Printing Existential Instances. \end{coq_eval} +Existential variables can be named by the user upon creation using +the syntax {\tt ?[\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{ltac:selector}). + \subsection{Explicit displaying of existential instances for pretty-printing \label{SetPrintingExistentialInstances} \optindex{Printing Existential Instances}} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 9378529cbe..9caea8f39b 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -392,7 +392,7 @@ all selected goals. \item{} [{\ident}] {\tt :} {\tacexpr} In this variant, {\tacexpr} is applied locally to a goal - previously named by the user. + previously named by the user (see~\ref{ExistentialVariables}). \item {\num} {\tt :} {\tacexpr} |