Documentation of records defined with the keywords Inductive and

CoInductive.

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

2 files changed, 23 insertions, 4 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index f0fb0883b..ce998a9bc 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -206,6 +206,7 @@
 %END LATEX
 %HEVEA \renewcommand{\proof}{\nterm{proof}}
 \newcommand{\record}{\nterm{record}}
+\newcommand{\recordkw}{\nterm{record\_keyword}}
 \newcommand{\rewrule}{\nterm{rewriting\_rule}}
 \newcommand{\sentence}{\nterm{sentence}}
 \newcommand{\simplepattern}{\nterm{simple\_pattern}}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 0cfdbe17b..2c4985c15 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -5,6 +5,8 @@ the Gallina's syntax.
 
 \section{Record types
 \comindex{Record}
+\comindex{Inductive}
+\comindex{CoInductive}
 \label{Record}}
 
 The \verb+Record+ construction is a macro allowing the definition of
@@ -20,10 +22,13 @@ construction allows to define ``signatures''.
 {\sentence} & ++= & {\record}\\
   & & \\
 {\record} & ::= &
-   {\tt Record} {\ident} \zeroone{\binders} \zeroone{{\tt :} {\sort}} \verb.:=. \\
+   {\recordkw} {\ident} \zeroone{\binders} \zeroone{{\tt :} {\sort}} \verb.:=. \\
 && ~~~~\zeroone{\ident}
        \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\
   & & \\
+{\recordkw} & ::= &
+   {\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\
+  & & \\
 {\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\
  & $|$ & {\name} \zeroone{\binders} {\typecstr} := {\term}
 \end{tabular}
@@ -149,6 +154,13 @@ Eval compute in half.(Rat_bottom_cond).
 Reset Initial.
 \end{coq_eval}
 
+Records defined  with the {\tt Record}  keyword are not  allowed to be
+recursive (references  to the record's name  in the type  of its field
+raises an  error). To define recursive  records, one can  use the {\tt
+  Inductive} and {\tt CoInductive} keywords, resulting in an inductive
+or  co-inductive record.  A  \emph{caveat}, however,  is that  records
+cannot appear in mutually inductive (or co-inductive) definitions.
+
 \begin{Warnings}
 \item {\tt Warning: {\ident$_i$} cannot be defined.}
 
@@ -167,10 +179,16 @@ Reset Initial.
 
 \begin{ErrMsgs}
 
-\item \errindex{A record cannot be recursive}
+\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.}
 
-  The record name {\ident} appears in the type of its fields.
-  
+  The record name {\ident} appears in the type of its fields, but uses
+  the keyword  {\tt Record}. Use  the keyword {\tt Inductive}  or {\tt
+    CoInductive} instead.
+\item \errindex{Cannot handle mutually (co)inductive records.}
+
+  Records  cannot  be  defined  as  part  of  mutually  inductive  (or
+  co-inductive) definitions,  whether with records only  or mixed with
+  standard definitions.
 \item During the definition of the one-constructor inductive
   definition, all the errors of inductive definitions, as described in
   Section~\ref{gal_Inductive_Definitions}, may also occur.