Document Generalizable Variables, and change syntax to

[Generalizable (All|No) Variables (ident+)?], also update 
type classes documentation to reflect the latest changes 
in instance decls. Fix a bug in [Util.list_split_when].


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12525 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 83 insertions, 27 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 23b018ee3..0ddbb6d89 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -47,6 +47,7 @@ record syntax of \Coq:
 \end{center}
 \begin{coq_eval}
   Reset Initial.
+  Generalizable All Variables.
 \end{coq_eval}
 
 The $\tele{\alpha_i : \tau_i}$ variables are called the \emph{parameters}
@@ -126,36 +127,21 @@ particular support for type classes:
   class arguments, making derived functions as easy to use as class
   methods. In the example above, \texttt{A} and \texttt{eqa} should be
   set maximally implicit.
-\item They support implicit quantification on class arguments and
-  partialy applied type classes (\S \ref{classes:impl-quant})
-\item They support implicit quantification on superclasses (\S \ref{classes:superclasses})
+\item They support implicit quantification on partialy applied type
+  classes (\S \ref{implicit-generalization}).
+  Any argument not given as part of a type class binder will be
+  automatically generalized.
+\item They also support implicit quantification on superclasses
+  (\S \ref{classes:superclasses})
 \end{itemize}
 
-\subsection{Implicit quantification}
-\label{classes:impl-quant}
-
-Implicit quantification is an automatic elaboration of a statement with
-free variables into a closed statement where these variables are
-quantified explicitly. Implicit generalization is done only inside
-binders beginning with a backquote \texttt{`} and the codomain of
-\texttt{Instance} declarations.
-
 Following the previous example, one can write:
 \begin{coq_example}
 Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 Here \texttt{A} is implicitly generalized, and the resulting function
-is equivalent to the one above. One must be careful that \emph{all} the
-free variables are generalized, which may result in confusing errors in
-case of typos. In such cases, the context will probably contain some
-unexpected generalized variable.
-
-The generalizing binders \verb|`{ }| and \verb|`( )| work similarly to 
-their explicit counterparts, only binding the generalized variables
-implicitly, as maximally-inserted arguments. In these binders, 
-the binding name for the bound object is optional, whereas the type is
-mandatory, dually to regular binders.
+is equivalent to the one above.
 
 \asection{Parameterized Instances}
 
@@ -311,7 +297,7 @@ parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to
   This variant declares a \emph{singleton} class whose only method is
   {\tt \ident$_1$}. This singleton class is a so-called definitional
   class, represented simply as a definition 
-  {\tt \ident \binder$_1$ \ldots \binder$_n$ := \type$_1$} and whose
+  {\tt {\ident} \binder$_1$ \ldots \binder$_n$ := \type$_1$} and whose
   instances are themselves objects of this type. Definitional classes
   are not wrapped inside records, and the trivial projection of an
   instance of such a class is convertible to the instance itself. This can
@@ -340,10 +326,12 @@ priority as for auto hints.
 
 \begin{Variants}
 \item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
+    forall {\binder$_{n+1}$ \ldots \binder$_m$},
     {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}] := \term} 
-  This syntax is used for declaration of singleton class instances. 
-  It does not include curly braces and one need not even mention
-  the unique field name.
+  This syntax is used for declaration of singleton class instances or
+  for directly giving an explicit term of type
+  {\tt forall {\binder$_{n+1}$ \ldots \binder$_m$}, {Class} {t$_1$ \ldots t$_n$}}.
+  One need not even mention the unique field name for singleton classes.
 
 \item {\tt Global Instance} One can use the \texttt{Global} modifier on
   instances declared in a section so that their generalization is automatically
@@ -409,5 +397,4 @@ based on a variant of eauto. The flags semantics are:
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
 %%% End: 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 3aa42dbd8..42374e368 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1483,6 +1483,9 @@ but succeeds in
 Check Prop = nat.
 \end{coq_example*}
 
+
+
+
 \subsection{Canonical structures
 \comindex{Canonical Structure}}
 
@@ -1584,6 +1587,72 @@ Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m.
 This is useful for declaring the implicit type of a single variable.
 \end{Variants}
 
+
+\subsection{Implicit generalization
+\label{implicit-generalization}
+\comindex{Generalizable Variables}}
+
+Implicit generalization is an automatic elaboration of a statement with
+free variables into a closed statement where these variables are
+quantified explicitly. Implicit generalization is done inside binders
+starting with a \verb|`| and terms delimited by \verb|`{ }| and
+\verb|`( )|, always introducing maximally inserted implicit arguments for
+the generalized variables. Inside implicit generalization
+delimiters, free variables in the current context are automatically
+quantified using a product or a lambda abstraction to generate a closed
+term. In the following statement for example, the variables \texttt{n}
+and \texttt{m} are autamatically generalized and become explicit
+arguments of the lemma as we are using \verb|`( )|:
+
+\begin{coq_example}
+Generalizable All Variables.
+Lemma nat_comm : `(n = n + 0).
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+One can control the set of generalizable identifiers with the
+\texttt{Generalizable} vernacular command to avoid unexpected
+generalizations when mistyping identifiers. There are three variants of
+the command:
+
+\begin{quote}
+{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.}
+\end{quote}
+
+\begin{Variants}
+\item {\tt Generalizable All Variables.} All variables are candidate for 
+  generalization if they appear free in the context under a
+  generalization delimiter. This may result in confusing errors in
+  case of typos. In such cases, the context will probably contain some
+  unexpected generalized variable.
+
+\item {\tt Generalizable No Variables.} Disable implicit generalization 
+  entirely. This is the default behavior.
+
+\item {\tt Generalizable Variable(s)? {\ident$_1$ \ident$_n$}.} 
+  Allow generalization of the given identifiers only. Calling this
+  command multiple times adds to the allowed identifiers.
+
+\item {\tt Global Generalizable} Allows to export the choice of
+  generalizable variables.
+\end{Variants}
+
+One can also use implicit generalization for binders, in which case the
+generalized variables are added as binders and set maximally implicit.
+\begin{coq_example*}
+Definition id `(x : A) : A := x.
+\end{coq_example*}
+\begin{coq_example}
+Print id.
+\end{coq_example}
+
+The generalizing binders \verb|`{ }| and \verb|`( )| work similarly to
+their explicit counterparts, only binding the generalized variables
+implicitly, as maximally-inserted arguments. In these binders, the
+binding name for the bound object is optional, whereas the type is
+mandatory, dually to regular binders.
+
 \section{Coercions
 \label{Coercions}
 \index{Coercions}}