From 14787df2ea09994151e886bf918aca0aecbd8ade Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Jan 2015 20:08:53 +0100
Subject: Reference Manual: Documenting new printing of evars and new effect of
 Set Printing Existential Instances (see bug report #3951).

---
 doc/refman/RefMan-ext.tex | 75 +++++++++++++++++++++++++++++++++--------------
 doc/refman/RefMan-pro.tex |  2 +-
 doc/refman/RefMan-tac.tex | 10 +++----
 3 files changed, 59 insertions(+), 28 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 2a976a07b3..193479cceb 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1929,30 +1929,60 @@ tools. The format is unspecified if {\str} doesn't end in
 \texttt{.dot} or \texttt{.gv}.
 
 \section[Existential variables]{Existential variables\label{ExistentialVariables}}
+\label{evars}
 
-Coq terms can include existential variables. An existential variable
-is a placeholder intended to eventually be replaced by an actual
-subterm though which subterm it will be replaced by is still unknown.
+Coq terms can include existential variables which
+represents unknown subterms to eventually be replaced by actual
+subterms.
 
 Existential variables are generated in place of unsolvable implicit
-arguments when using commands such as \texttt{Check} (see
-Section~\ref{Check}) or in place of unsolvable instances when using
-tactics such as \texttt{eapply} (see Section~\ref{eapply}). They can
-only appear as the result of a command displaying a term and they are
-represented by ``?'' followed by a number. They cannot be entered by
-the user (though they can be generated from ``\_'' when the
-corresponding implicit argument is unsolvable).
-
-A given existential variable name can occur several times in a term
-meaning the corresponding expected instance is shared. Each
-existential variable is relative to a context, as shown by {\tt Show
-  Existential} when in the process of proving a goal (see
-Section~\ref{ShowExistentials}). Henceforth, each occurrence of an
-existential variable in a term is subject to an instance of the
-variables of its context of definition which is specific to this
-occurrence.
+arguments or ``{\tt \_}'' placeholders when using commands such as
+\texttt{Check} (see Section~\ref{Check}) or when using tactics such as
+\texttt{refine}~(see Section~\ref{refine}), as well as in place of unsolvable
+instances when using tactics such that \texttt{eapply} (see
+Section~\ref{eapply}). An existential variable is defined in a
+context, which is the context of variables of the placeholder which
+generated the existential variable, and a type, which is the expected
+type of the placeholder. 
+
+As a consequence of typing constraints, existential variables can be
+duplicated in such a way that they possibly appear in different
+contexts than their defining context. Thus, any occurrence of a given
+existential variable comes with an instance of its original context. In the
+simple case, when an existential variable denotes the placeholder
+which generated it, or is used in the same context as the one in which
+it was generated, the context is not displayed and the existential
+variable is represented by ``?'' followed by an identifier.
+
+\begin{coq_example}
+Parameter identity : forall (X:Set), X -> X.
+Check identity _ _.
+Check identity _ (fun x => _).
+\end{coq_example}
+
+In the general case, when an existential variable ?{\ident}
+appears outside of its context of definition, its instance, written under
+the form \verb!@{id1:=term1; ...; idn:=termn}!, is appending to its
+name, indicating how the variables of its defining context are
+instantiated.  The variables of the context of the existential
+variables which are instantiated by themselves are not written, unless
+the flag {\tt Printing Existential Instances} is on (see
+Section~\ref{SetPrintingExistentialInstances}), and this is why an
+existential variable used in the same context as its context of
+definition is written with no instance.
+
+\begin{coq_example}
+Check (fun x y => _) 0 1.
+Set Printing Existential Instances.
+Check (fun x y => _) 0 1.
+\end{coq_example}
+
+\begin{coq_eval}
+Unset Printing Existential Instances.
+\end{coq_eval}
 
 \subsection{Explicit displaying of existential instances for pretty-printing
+\label{SetPrintingExistentialInstances}
 \comindex{Set Printing Existential Instances}
 \comindex{Unset Printing Existential Instances}}
 
@@ -1960,10 +1990,11 @@ The command:
 \begin{quote}
 {\tt Set Printing Existential Instances}
 \end{quote}
-activates the display of how the context of an existential variable is
-instantiated on each of its occurrences.
+activates the full display of how the context of an existential variable is
+instantiated at each of the occurrences of the existential variable.
 
-To deactivate the display of the instances of existential variables, use
+To deactivate the full display of the instances of existential
+variables, use
 \begin{quote}
 {\tt Unset Printing Existential Instances.}
 \end{quote}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index eabb376395..df707ce941 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -239,7 +239,7 @@ proof was edited.
 
 This command instantiates an existential variable. {\tt \num}
 is an index in the list of uninstantiated existential variables
-displayed by {\tt Show Existentials.} (described in Section~\ref{Show})
+displayed by {\tt Show Existentials} (described in Section~\ref{Show}).
 
 This command is intended to be used to instantiate existential
 variables when the proof is completed but some uninstantiated
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1b7adc2517..35da17d546 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -260,6 +260,7 @@ Defined.
 \subsection{\tt apply \term}
 \tacindex{apply}
 \label{apply}
+\label{eapply}
 
 This tactic applies to any goal.  The argument {\term} is a term
 well-formed in the local context.  The tactic {\tt apply} tries to
@@ -329,14 +330,13 @@ Section~\ref{pattern} to transform the goal so that it gets the form
    generated by {\tt apply} {\term$_i$}, starting from the application
    of {\term$_1$}.
 
-\item {\tt eapply \term}\tacindex{eapply}\label{eapply}
+\item {\tt eapply \term}\tacindex{eapply}
 
   The tactic {\tt eapply} behaves like {\tt apply} but it does not fail
   when no instantiations are deducible for some variables in the
-  premises.  Rather, it turns these variables into so-called
-  existential variables which are variables still to instantiate. An
-  existential variable is identified by a name of the form {\tt ?$n$}
-  where $n$ is a number.  The instantiation is intended to be found
+  premises. Rather, it turns these variables into 
+  existential variables which are variables still to instantiate (see
+  Section~\ref{evars}). The instantiation is intended to be found
   later in the proof.
 
 \item {\tt simple apply {\term}} \tacindex{simple apply}
-- 
cgit v1.2.3