From 39f36789b986779d36acd36cfa1425487bad43c3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 12:27:18 +0200
Subject: Document evar naming syntax.

---
 doc/refman/RefMan-ext.tex | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'doc/refman/RefMan-ext.tex')

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}}
-- 
cgit v1.2.3