From 4e8b2db573752ff7376ec74f3b5c5a5beebb3e7d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Mar 2004 19:46:59 +0000
Subject: Quelques erreurs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8499 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-gal.tex | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index e856566c7b..0696f17020 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 :=
-- 
cgit v1.2.3