Last changes in type class syntax:

- curly braces mandatory for record class instances
- no mention of the unique method for definitional class instances
Turning a record or definition into a class is mostly a 
matter of changing the keywords to 'Class' and 'Instance' now.
Documentation reflects these changes, and was checked once more 
along with setoid_rewrite's and Program's.


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

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 502b42b837..8b404f4efa 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -24,7 +24,7 @@ construction allows to define ``signatures''.
 && ~~~~\zeroone{\ident}
        \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\
   & & \\
-{\field} & ::= & {\name} : {\type} \\
+{\field} & ::= & {\name} : {\type} [ {\tt where} {\it notation} ] \\
  & $|$ & {\name} {\typecstr} := {\term}
 \end{tabular}
 \end{centerframe}