Documenting the [Variant] type definition and the [Nonrecursive Elimination Schemes] option.

3 files changed, 33 insertions, 4 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index ef4829515..970347422 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -97,9 +97,9 @@ Remark here that the field
 %\medskip
 
 Let us now see the work done by the {\tt Record} macro.  First the
-macro generates an inductive definition with just one constructor:
+macro generates a variant type definition with just one constructor:
 \begin{quote}
-{\tt Inductive {\ident} {\params} :{\sort} :=} \\
+{\tt Variant {\ident} {\params} :{\sort} :=} \\
 \qquad {\tt
   {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).}
 \end{quote}
@@ -160,6 +160,11 @@ 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.
+Induction schemes are automatically generated for inductive records.
+Automatic generation of induction schemes for non-recursive records
+defined with the {\tt Record} keyword can be activated with the
+{\tt Nonrecursive Elimination Schemes} option
+(see~\ref{set-nonrecursive-elimination-schemes}).
 
 \begin{Warnings}
 \item {\tt Warning: {\ident$_i$} cannot be defined.}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index b8e715c76..63440f4de 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -929,7 +929,9 @@ section and depending on {\ident} are prefixed by the let-in definition
 \index{Inductive definitions}
 \label{gal-Inductive-Definitions}
 \comindex{Inductive}
-\label{Inductive}}
+\label{Inductive}
+\comindex{Variant}
+\label{Variant}}
 
 We gradually explain simple inductive types, simple
 annotated inductive types, simple parametric inductive types, 
@@ -1107,6 +1109,16 @@ Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
 \end{coq_example*}
 This is an alternative definition of lists where we specify the
 arguments of the constructors rather than their full type.
+\item
+\begin{coq_example*}
+Variant sum (A B:Set) : Set := left : A->sum A B | right : B->Sum A B.
+\end{coq_example*}
+The {\tt Variant} keyword is identical to the {\tt Inductive} keyword,
+except that it disallows recursive definition of types (in particular
+lists cannot be defined with the {\tt Variant} keyword). No induction
+scheme is generated for this variant, unless the option
+{\tt Nonrecursive Elimination Schemes} is set
+(see~\ref{set-nonrecursive-elimination-schemes}).
 \end{Variants}
 
 \begin{ErrMsgs}
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index c80e3ceeb..e28e4a443 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -122,14 +122,26 @@ Check odd_even.
 The type of {\tt even\_odd} shares the same premises but the
 conclusion is {\tt (n:nat)(even n)->(Q n)}.
 
-\subsection{Automatic declaration of schemes}
+\subsection{Automatic declaration of schemes
 \comindex{Set Boolean Equality Schemes}
+\comindex{Unset Boolean Equality Schemes}
 \comindex{Set Elimination Schemes}
+\comindex{Unset Elimination Schemes}
+\comindex{Set Nonrecursive Elimination Schemes}
+\comindex{Unset Nonrecursive Elimination Schemes}
+\label{set-nonrecursive-elimination-schemes}
+}
 
 It is possible to deactivate the automatic declaration of the induction
  principles when defining a new inductive type  with the
  {\tt Unset Elimination Schemes} command. It may be
 reactivated at any time with {\tt Set Elimination Schemes}.
+
+The types declared with the keywords {\tt Variant} (see~\ref{Variant})
+and {\tt Record} (see~\ref{Record}) do not have an automatic
+declaration of the induction principles. It can be activated with the
+command {\tt Set Nonrecursive Elimination Schemes}. It can be
+deactivated again with {\tt Unset Nonrecursive Elimination Schemes}.
 \\
 
 You can also activate the automatic declaration of those boolean equalities