From 895fcffc774abada4677d52a7dbbb54a85cadec7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 18 Jan 2009 17:36:51 +0000
Subject: 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
---
 doc/refman/RefMan-ext.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-ext.tex')

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}
-- 
cgit v1.2.3