diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 19:46:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 19:46:59 +0000 |
| commit | 4e8b2db573752ff7376ec74f3b5c5a5beebb3e7d (patch) | |
| tree | 8478d41dadabf240acb61d5a13ae4305e36591c4 | |
| parent | 31ed89d3a0f0435edfe064bbe26ce810d7f6494f (diff) | |
Quelques erreurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8499 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/RefMan-gal.tex | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index e856566c7..0696f1702 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -963,7 +963,7 @@ Reset Initial. \begin{Variants} \item \begin{coq_example*} -Inductive list (A:Set) : Set := nil | cons (_:X) (_:list X). +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. @@ -1036,6 +1036,9 @@ The typical example of a mutual inductive data type is the one for trees and forests. We assume given two types $A$ and $B$ as variables. It can be declared the following way. +\begin{coq_eval} +Reset Initial. +\end{coq_eval} \begin{coq_example*} Variables A B : Set. Inductive tree : Set := |