1 files changed, 18 insertions, 7 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 7bd4f352..f427609f 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -10,7 +10,7 @@
 \label{typeclasses}
 
 \begin{flushleft}
-  \em The status of Type Classes is (extremely) experimental.
+  \em The status of Type Classes is experimental.
 \end{flushleft}
 
 This chapter presents a quick reference of the commands related to type
@@ -128,9 +128,7 @@ particular support for type classes:
   methods. In the example above, \texttt{A} and \texttt{eqa} should be
   set maximally implicit.
 \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.
+  classes.
 \item They also support implicit quantification on superclasses
   (\S \ref{classes:superclasses})
 \end{itemize}
@@ -143,6 +141,19 @@ Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
 Here \texttt{A} is implicitly generalized, and the resulting function
 is equivalent to the one above.
 
+The parsing of generalized type-class binders is different from regular
+binders:
+\begin{itemize}
+\item Implicit arguments of the class type are ignored.
+\item Superclasses arguments are automatically generalized.
+\item Any remaining arguments not given as part of a type class binder
+  will be automatically generalized. In other words, the rightmost
+  parameters are automatically generalized if not mentionned.
+\end{itemize}
+
+One can switch off this special treatment using the $!$ mark in front of
+the class name (see example below).
+
 \asection{Parameterized Instances}
 
 One can declare parameterized instances as in \Haskell simply by giving
@@ -231,9 +242,9 @@ Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x).
 \end{coq_example*}
 
 In some cases, to be able to specify sharing of structures, one may want to give
-explicitly the superclasses. It is is possible to do it directly in regular
-binders, and using the \texttt{!} modifier in class binders. For
-example:
+explicitly the superclasses. It is possible to do it directly in regular
+generalized binders, and using the \texttt{!} modifier in class
+binders. For example:
 \begin{coq_example*}
 Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := 
   andb (le x y) (neqb x y).