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

5 files changed, 90 insertions, 32 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}}
diff --git a/lib/util.ml b/lib/util.ml
index 9f29d55bd..5e2a071a9 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -810,7 +810,7 @@ let list_split_at index l =
 let list_split_when p =
   let rec split_when_loop x y =
     match y with
-      | []      -> ([],[])
+      | []      -> (List.rev x,[])
       | (a::l)  -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l
   in
   split_when_loop []
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a0ee06683..3bc27965a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -553,9 +553,11 @@ GEXTEND Gram
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c)
 
-      | IDENT "Generalizable"; ["Variable" | IDENT "Variables"];
-           gen = [ IDENT "none" -> None | IDENT "all" -> Some [] | 
-	       idl = LIST1 identref -> Some idl ] ->
+      | IDENT "Generalizable"; 
+	   gen = [IDENT "All"; IDENT "Variables" -> Some []
+	     | IDENT "No"; IDENT "Variables" -> None
+	     | [IDENT "Variable" | IDENT "Variables"];
+		  idl = LIST1 identref -> Some idl ] ->
 	     VernacGeneralizable (use_non_locality (), gen) ] ]
   ;
   implicit_name:
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index ac455415e..f5d08edb4 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -20,7 +20,7 @@ Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
-Generalizable Variables all.
+Generalizable All Variables.
 
 (** * Morphisms.