diff options
| author | Maxime Dénès | 2017-06-16 08:42:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-16 08:42:57 +0200 |
| commit | c22fe8bb7e0fedd8b3ced088832c13b5e55e9fc2 (patch) | |
| tree | 42de8d4e25a46ef27fa105652d8cae5b5bcb60c1 /doc/refman/RefMan-ext.tex | |
| parent | f8e3a9ac43ec50a5810cd7835fa562918db0bdcb (diff) | |
| parent | 5636fc49828f6007a8b756cd0517280a73147da6 (diff) | |
Merge PR#767: Document named evars (including Show ident)
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 5 |
1 files changed, 5 insertions, 0 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}} |