Merge branch 'v8.6'

6 files changed, 204 insertions, 180 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index acfc4bea9..5966ac468 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -554,7 +554,7 @@ more efficient resolution behavior (the option is off by default). When
 a solution to the typeclass goal of this class is found, we never
 backtrack on it, assuming that it is canonical.
 
-\subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]}
+\subsection{\tt Typeclasses eauto := [debug] [(dfs) | (bfs)] [\emph{depth}]}
 \comindex{Typeclasses eauto}
 \label{TypeclassesEauto}
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 939fc87a6..f338c3055 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -38,21 +38,19 @@ construction allows defining ``signatures''.
 \end{figure}
 
 \noindent In the expression
-
-\smallskip
-{\tt Record} {\ident} {\params} \texttt{:} 
-   {\sort} := {\ident$_0$} \verb+{+
- {\ident$_1$} \binders$_1$ \texttt{:} {\term$_1$}; 
-              \dots
-  {\ident$_n$} \binders$_n$ \texttt{:} {\term$_n$} \verb+}+.
-\smallskip
- 
+\begin{quote}
+{\tt Record {\ident} {\params} : {\sort} := {\ident$_0$} \{ \\
+  {\ident$_1$} \binders$_1$ : {\term$_1$} ; ... ; \\
+  {\ident$_n$} \binders$_n$ : {\term$_n$} \}.}
+\end{quote}
 \noindent the identifier {\ident} is the name of the defined record
 and {\sort} is its type. The identifier {\ident$_0$} is the name of
 its constructor. If {\ident$_0$} is omitted, the default name {\tt
-Build\_{\ident}} is used. If {\sort} is omitted, the default sort is ``{\Type}''.
-The identifiers {\ident$_1$}, ..,
-{\ident$_n$} are the names of fields and {\tt forall} \binders$_1${\tt ,} {\term$_1$}, ..., {\tt forall} \binders$_n${\tt ,} {\term$_n$}
+Build\_{\ident}} is used.
+If {\sort} is omitted, the default sort is {\Type}.
+The identifiers {\ident$_1$}, \dots, {\ident$_n$} are the names of
+fields and {\tt forall {\binders$_1$}, {\term$_1$}}, \dots,
+{\tt forall {\binders$_n$}, {\term$_n$}}
 their respective types. Remark that the type of {\ident$_i$} may
 depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the
 fields is important. Finally, {\params} are the parameters of the
@@ -82,26 +80,15 @@ Record Rat : Set := mkRat
     forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}.
 \end{coq_example}
 
-Remark here that the field
-\verb+Rat_cond+ depends on the field \verb+bottom+. 
-
-%Let us now see the work done by the {\tt Record} macro.
-%First the macro generates an inductive definition
-%with just one constructor:
-%
-%\medskip
-%\noindent
-%{\tt Inductive {\ident} \zeroone{\binders} : {\sort} := \\
-%\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. 
-%({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.}
-%\medskip
+Remark here that the field \verb+Rat_bottom_cond+ depends
+on the field \verb+bottom+ and \verb+Rat_irred_cond+ depends
+on both \verb+top+ and \verb+bottom+.
 
 Let us now see the work done by the {\tt Record} macro.  First the
 macro generates a variant type definition with just one constructor:
 \begin{quote}
-{\tt Variant {\ident} {\params} :{\sort} :=} \\
-\qquad {\tt
-  {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).}
+{\tt Variant {\ident} {\params} : {\sort} := \\
+  {\ident$_0$} ({\ident$_1$} : {\term$_1$}) ... ({\ident$_n$} : {\term$_n$}).}
 \end{quote}
 To build an object of type {\ident}, one should provide the
 constructor {\ident$_0$} with $n$ terms filling the fields of
@@ -109,28 +96,9 @@ the record.
 
 As an example, let us define the rational $1/2$:
 \begin{coq_example*}
-Require Import Arith.
 Theorem one_two_irred :
  forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1.
-\end{coq_example*}
-\begin{coq_eval}
-Lemma mult_m_n_eq_m_1 : forall m n:nat, m * n = 1 -> m = 1.
-destruct m; trivial.
-intros; apply f_equal with (f := S).
-destruct m; trivial.
-destruct n; simpl in H.
- rewrite <- mult_n_O in H.
-   discriminate.
- rewrite <- plus_n_Sm in H.
-   discriminate.
-Qed.
-
-intros x y z [H1 H2].
- apply mult_m_n_eq_m_1 with (n := y); trivial.
-\end{coq_eval}
-\ldots
-\begin{coq_example*}
-Qed.
+Admitted.
 \end{coq_example*}
 \begin{coq_example}
 Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
@@ -139,80 +107,6 @@ Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
 Check half.
 \end{coq_example}
 
-The macro generates also, when it is possible, the projection
-functions for destructuring an object of type {\ident}.  These
-projection functions have the same name that the corresponding
-fields. If a field is named ``\verb=_='' then no projection is built
-for it.  In our example:
-
-\begin{coq_example}
-Eval compute in half.(top).
-Eval compute in half.(bottom).
-Eval compute in half.(Rat_bottom_cond).
-\end{coq_example}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-Records defined  with the {\tt Record}  keyword are not  allowed to be
-recursive (references  to the record's name  in the type  of its field
-raises an  error). To define recursive  records, one can  use the {\tt
-  Inductive} and {\tt CoInductive} keywords, resulting in an inductive
-or  co-inductive record.  A  \emph{caveat}, however,  is that  records
-cannot appear in mutually inductive (or co-inductive) definitions.
-Induction schemes are automatically generated for inductive records.
-Automatic generation of induction schemes for non-recursive records
-defined with the {\tt Record} keyword can be activated with the
-{\tt Nonrecursive Elimination Schemes} option
-(see~\ref{set-nonrecursive-elimination-schemes}).
-
-\begin{Warnings}
-\item {\tt {\ident$_i$} cannot be defined.}
-
-  It can happen that the definition of a projection is impossible.
-  This message is followed by an explanation of this impossibility.
-  There may be three reasons:
-   \begin{enumerate}
-   \item The name {\ident$_i$} already exists in the environment (see
-     Section~\ref{Axiom}).
-   \item The body of {\ident$_i$} uses an incorrect elimination for
-     {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}).
-   \item The type of the projections {\ident$_i$} depends on previous
-   projections which themselves could not be defined.
-   \end{enumerate}  
-\end{Warnings}     
-
-\begin{ErrMsgs}
-
-\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.}
-
-  The record name {\ident} appears in the type of its fields, but uses
-  the keyword  {\tt Record}. Use  the keyword {\tt Inductive}  or {\tt
-    CoInductive} instead.
-\item \errindex{Cannot handle mutually (co)inductive records.}
-
-  Records  cannot  be  defined  as  part  of  mutually  inductive  (or
-  co-inductive) definitions,  whether with records only  or mixed with
-  standard definitions.
-\item During the definition of the one-constructor inductive
-  definition, all the errors of inductive definitions, as described in
-  Section~\ref{gal-Inductive-Definitions}, may also occur.
-
-\end{ErrMsgs}
-
-\SeeAlso Coercions and records in Section~\ref{Coercions-and-records}
-of the chapter devoted to coercions.
-
-\Rem {\tt Structure} is a synonym of the keyword {\tt Record}.
-
-\Rem Creation of an object of record type can be done by calling {\ident$_0$}
-and passing arguments in the correct order.
-
-\begin{coq_example}
-Record point := { x : nat; y : nat }.
-Definition a := Build_point 5 3.
-\end{coq_example}
-
 \begin{figure}[t]
 \begin{centerframe}
 \begin{tabular}{lcl}
@@ -226,15 +120,17 @@ Definition a := Build_point 5 3.
 \label{fig:fieldsyntax}
 \end{figure}
 
-A syntax is available for creating objects by using named fields, as
+Alternatively, the following syntax allows creating objects by using named fields, as
 shown on Figure~\ref{fig:fieldsyntax}. The
 fields do not have to be in any particular order, nor do they have to be all
 present if the missing ones can be inferred or prompted for (see
 Section~\ref{Program}).
 
 \begin{coq_example}
-Definition b := {| x := 5; y := 3 |}.
-Definition c := {| y := 3; x := 5 |}.
+Definition half' :=
+  {| sign := true;
+     Rat_bottom_cond := O_S 1;
+     Rat_irred_cond := one_two_irred |}.
 \end{coq_example}
 
 This syntax can be disabled globally for printing by
@@ -256,23 +152,52 @@ This syntax can also be used for pattern matching.
 
 \begin{coq_example}
 Eval compute in (
-  match b with
-  | {| y := S n |} => n
+  match half with
+  | {| sign := true; top := n |} => n
   | _ => 0
   end).
 \end{coq_example}
 
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
+The macro generates also, when it is possible, the projection
+functions for destructuring an object of type {\ident}.  These
+projection functions are given the names of the corresponding
+fields. If a field is named ``\verb=_='' then no projection is built
+for it. In our example:
+
+\begin{coq_example}
+Eval compute in top half.
+Eval compute in bottom half.
+Eval compute in Rat_bottom_cond half.
+\end{coq_example}
+
+An alternative syntax for projections based on a dot notation is
+available:
+
+\begin{coq_example}
+Eval compute in half.(top).
+\end{coq_example}
 
-\Rem A syntax for projections based on a dot notation is
-available. The command to activate it is
+It can be activated for printing with the command
 \optindex{Printing Projections}
 \begin{quote}
 {\tt Set Printing Projections.}
 \end{quote}
 
+\begin{coq_example}
+Set Printing Projections.
+Check top half.
+\end{coq_example}
+
+The corresponding grammar rules are given in Figure~\ref{fig:projsyntax}.
+When {\qualid} denotes a projection, the syntax {\tt
+  {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax
+{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to
+{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax
+{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to
+{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term}
+is the object projected and the other arguments are the parameters of
+the inductive type.
+
 \begin{figure}[t]
 \begin{centerframe}
 \begin{tabular}{lcl}
@@ -285,18 +210,66 @@ available. The command to activate it is
 \label{fig:projsyntax}
 \end{figure}
 
-The corresponding grammar rules are given Figure~\ref{fig:projsyntax}.
-When {\qualid} denotes a projection, the syntax {\tt
-  {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax
-{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to
-{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax
-{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to
-{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term}
-is the object projected and the other arguments are the parameters of
-the inductive type.
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{Remarks}
+
+\item Records defined with the {\tt Record} keyword are not allowed to be
+recursive (references to the record's name in the type of its field
+raises an  error). To define recursive records, one can use the {\tt
+Inductive} and {\tt CoInductive} keywords, resulting in an inductive
+or co-inductive record.
+A \emph{caveat}, however, is that records
+cannot appear in mutually inductive (or co-inductive) definitions.
+
+\item Induction schemes are automatically generated for inductive records.
+Automatic generation of induction schemes for non-recursive records
+defined with the {\tt Record} keyword can be activated with the
+{\tt Nonrecursive Elimination Schemes} option
+(see~\ref{set-nonrecursive-elimination-schemes}).
+
+\item {\tt Structure} is a synonym of the keyword {\tt Record}.
 
-To deactivate the printing of projections, use 
-{\tt Unset Printing Projections}.
+\end{Remarks}
+
+\begin{Warnings}
+\item {\tt {\ident$_i$} cannot be defined.}
+
+  It can happen that the definition of a projection is impossible.
+  This message is followed by an explanation of this impossibility.
+  There may be three reasons:
+   \begin{enumerate}
+   \item The name {\ident$_i$} already exists in the environment (see
+     Section~\ref{Axiom}).
+   \item The body of {\ident$_i$} uses an incorrect elimination for
+     {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}).
+   \item The type of the projections {\ident$_i$} depends on previous
+   projections which themselves could not be defined.
+   \end{enumerate}  
+\end{Warnings}     
+
+\begin{ErrMsgs}
+
+\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.}
+
+  The record name {\ident} appears in the type of its fields, but uses
+  the keyword  {\tt Record}. Use  the keyword {\tt Inductive}  or {\tt
+    CoInductive} instead.
+\item \errindex{Cannot handle mutually (co)inductive records.}
+
+  Records  cannot  be  defined  as  part  of  mutually  inductive  (or
+  co-inductive) definitions,  whether with records only  or mixed with
+  standard definitions.
+\item During the definition of the one-constructor inductive
+  definition, all the errors of inductive definitions, as described in
+  Section~\ref{gal-Inductive-Definitions}, may also occur.
+
+\end{ErrMsgs}
+
+\SeeAlso Coercions and records in Section~\ref{Coercions-and-records}
+of the chapter devoted to coercions.
 
 \subsection{Primitive Projections}
 \optindex{Primitive Projections}
@@ -2011,6 +1984,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 bb679ecba..f3bc2dd05 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}
 
@@ -891,7 +891,7 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag.
 
 \end{Variants}
 
-\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}
+\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal}
 \index{Ltac!match reverse goal@\texttt{match reverse goal}}
 \index{match goal@\texttt{match goal}!in Ltac}
 \index{match reverse goal@\texttt{match reverse goal}!in Ltac}}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index b66659dc8..95fee3241 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -421,6 +421,24 @@ This command displays the current goals.
 \item \errindex{No focused proof}
 \end{ErrMsgs}
 
+\item {\tt Show {\ident}.}\\
+  Displays the named goal {\ident}.
+  This is useful in particular to display a shelved goal but only works
+  if the corresponding existential variable has been named by the user
+  (see~\ref{ExistentialVariables}) as in the following example.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Goal exists n, n = 0.
+  eexists ?[n].
+\end{coq_example*}
+\begin{coq_example}
+  Show n.
+\end{coq_example}
+
 \item {\tt Show Script.}\comindex{Show Script}\\
   Displays the whole list of tactics applied from the beginning
   of the current proof. 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index ecaf82806..d02b06df1 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -889,7 +889,8 @@ statically. For instance, if {\tt f} is a polymorphic function of type
 recognized as an argument to be interpreted in scope {\scope}.
 
 \comindex{Bind Scope}
-More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
+\label{bindscope}
+More generally, any coercion {\class} (see Chapter~\ref{Coercions-full}) can be
 bound to an interpretation scope. The command to do it is
 \begin{quote}
 {\tt Bind Scope} {\scope} \texttt{with} {\class}
@@ -908,7 +909,7 @@ Open Scope nat_scope. (* Define + on the nat as the default for + *)
 Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))).
 \end{coq_example}
 
-\Rem The scope {\tt type\_scope} has also a local effect on
+\Rem The scopes {\tt type\_scope} and {\tt function\_scope} also have a local effect on
 interpretation. See the next section.
 
 \SeeAlso The command to show the scopes bound to the arguments of a
@@ -940,10 +941,21 @@ Check # @@%mybool #.
 
 The scope {\tt type\_scope} has a special status. It is a primitive
 interpretation scope which is temporarily activated each time a
-subterm of an expression is expected to be a type. This includes goals
-and statements, types of binders, domain and codomain of implication,
-codomain of products, and more generally any type argument of a
-declared or defined constant.
+subterm of an expression is expected to be a type.  It is delimited by
+the key {\tt type}, and bound to the coercion class {\tt Sortclass}. It is also
+used in certain situations where an expression is statically known to
+be a type, including the conclusion and the type of hypotheses within
+an {\tt Ltac} goal match (see Section~\ref{ltac-match-goal})
+the statement of a theorem, the type of
+a definition, the type of a binder, the domain and codomain of
+implication, the codomain of products, and more generally any type
+argument of a declared or defined constant.
+
+\subsection[The {\tt function\_scope} interpretation scope]{The {\tt function\_scope} interpretation scope\index{function\_scope@\texttt{function\_scope}}}
+
+The scope {\tt function\_scope} also has a special status. 
+It is temporarily activated each time the argument of a global reference is
+recognized to be a {\tt Funclass instance}, i.e., of type {\tt forall x:A, B} or {\tt A -> B}.
 
 \subsection{Interpretation scopes used in the standard library of {\Coq}}
 
@@ -953,38 +965,39 @@ commands {\tt Print Scopes} or {\tt Print Scope {\scope}}.
 
 \subsubsection{\tt type\_scope}
 
-This includes infix {\tt *} for product types and infix {\tt +} for
-sum types. It is delimited by key {\tt type}.
+This scope includes infix {\tt *} for product types and infix {\tt +} for
+sum types. It is delimited by key {\tt type}, and bound to the coercion class 
+{\tt Sortclass}, as described at \ref{bindscope}.
 
 \subsubsection{\tt nat\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt nat}. Positive numerals in this scope are mapped to their
 canonical representent built from {\tt O} and {\tt S}. The scope is
-delimited by key {\tt nat}.
+delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}).
 
 \subsubsection{\tt N\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt N} (binary natural numbers). It is delimited by key {\tt N}
 and comes with an interpretation for numerals as closed term of type {\tt Z}.
 
 \subsubsection{\tt Z\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt Z} (binary integer numbers). It is delimited by key {\tt Z} 
 and comes with an interpretation for numerals as closed term of type {\tt Z}.
 
 \subsubsection{\tt positive\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt positive} (binary strictly positive numbers). It is
 delimited by key {\tt positive} and comes with an interpretation for
 numerals as closed term of type {\tt positive}.
 
 \subsubsection{\tt Q\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt Q} (rational numbers defined as fractions of an integer and
 a strictly positive integer modulo the equality of the
 numerator-denominator cross-product). As for numerals, only $0$ and
@@ -993,13 +1006,13 @@ interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively).
 
 \subsubsection{\tt Qc\_scope}
 
-This includes the standard arithmetical operators and relations on the
+This scope includes the standard arithmetical operators and relations on the
 type {\tt Qc} of rational numbers defined as the type of irreducible
 fractions of an integer and a strictly positive integer.
 
 \subsubsection{\tt real\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R}
 and comes with an interpretation for numerals as term of type {\tt
 R}. The interpretation is based on the binary decomposition.  The
@@ -1014,35 +1027,40 @@ those of {\tt R}.
 
 \subsubsection{\tt bool\_scope}
 
-This includes notations for the boolean operators. It is
-delimited by key {\tt bool}.
+This scope includes notations for the boolean operators. It is
+delimited by key {\tt bool}, and bound to the type {\tt bool} (see \ref{bindscope}).
 
 \subsubsection{\tt list\_scope}
 
-This includes notations for the list operators. It is
-delimited by key {\tt list}.
+This scope includes notations for the list operators. It is
+delimited by key {\tt list}, and bound to the type {\tt list} (see \ref{bindscope}).
+
+\subsubsection{\tt function\_scope}
+
+This scope is delimited by the key {\tt function}, and bound to the coercion class {\tt Funclass}, 
+as described at \ref{bindscope}.
 
 \subsubsection{\tt core\_scope}
 
-This includes the notation for pairs. It is delimited by key {\tt core}.
+This scope includes the notation for pairs. It is delimited by key {\tt core}.
 
 \subsubsection{\tt string\_scope}
 
-This includes notation for strings as elements of the type {\tt
+This scope includes notation for strings as elements of the type {\tt
 string}.  Special characters and escaping follow {\Coq} conventions
 on strings (see Section~\ref{strings}). Especially, there is no
 convention to visualize non printable characters of a string.  The
 file {\tt String.v} shows an example that contains quotes, a newline
-and a beep (i.e. the ascii character of code 7).
+and a beep (i.e. the ASCII character of code 7).
 
 \subsubsection{\tt char\_scope}
 
-This includes interpretation for all strings of the form
-\verb!"!$c$\verb!"! where $c$ is an ascii character, or of the form
+This scope includes interpretation for all strings of the form
+\verb!"!$c$\verb!"! where $c$ is an ASCII character, or of the form
 \verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly
 with leading 0's), or of the form \verb!""""!. Their respective
-denotations are the ascii code of $c$, the decimal ascii code $nnn$,
-or the ascii code of the character \verb!"! (i.e. the ascii code
+denotations are the ASCII code of $c$, the decimal ASCII code $nnn$,
+or the ASCII code of the character \verb!"! (i.e. the ASCII code
 34), all of them being represented in the type {\tt ascii}.
 
 \subsection{Displaying informations about scopes}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index be75dc9d5..4931ca3b6 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1515,23 +1515,33 @@ The {\tt evar} tactic creates a new local definition named \ident\ with
 type \term\ in the context. The body of this binding is a fresh
 existential variable.
 
-\subsection{\tt instantiate ( {\num} := {\term} )}
+\subsection{\tt instantiate ( {\ident} := {\term} )}
 \tacindex{instantiate}
 \label{instantiate}
 
 The {\tt instantiate} tactic refines (see Section~\ref{refine})
-an existential variable
-with the term \term. The \num\  argument is the position of the
-existential variable from right to left in the conclusion. This cannot be
-the number of the existential variable since this number is different
-in every session.
+an existential variable {\ident} with the term {\term}.
+It is equivalent to {\tt only [\ident]: refine \term} (preferred alternative).
 
-When you are referring to hypotheses which you did not name
+\begin{Remarks}
+\item To be able to refer to an existential variable by name, the
+user must have given the name explicitly (see~\ref{ExistentialVariables}).
+
+\item When you are referring to hypotheses which you did not name
 explicitly, be aware that Coq may make a different decision on how to
 name the variable in the current goal and in the context of the
 existential variable. This can lead to surprising behaviors.
+\end{Remarks}
 
 \begin{Variants}
+
+  \item {\tt instantiate ( {\num} := {\term} )}
+  This variant allows to refer to an existential variable which was not
+  named by the user. The {\num} argument is the position of the
+  existential variable from right to left in the goal.
+  Because this variant is not robust to slight changes in the goal,
+  its use is strongly discouraged.
+
   \item {\tt instantiate ( {\num} := {\term} ) in \ident}
 
   \item {\tt instantiate ( {\num} := {\term} ) in ( Value of {\ident} )}