From df7ee5401f9010ca659da7bdb11cf85f3c79021b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 5 Jan 2004 19:11:26 +0000
Subject: MAJ pour compilation coq-tex correcte

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

(limited to 'doc/RefMan-mod.tex')

diff --git a/doc/RefMan-mod.tex b/doc/RefMan-mod.tex
index 490d21fd8e..9f6f2abce1 100644
--- a/doc/RefMan-mod.tex
+++ b/doc/RefMan-mod.tex
@@ -226,6 +226,11 @@ Now we can create a new module from \texttt{M}, giving it a less
 precise specification: the \texttt{y} component is dropped as well
 as the body of \texttt{x}.
 
+\begin{coq_eval}
+Set Printing Depth 50.
+(********** The following is not correct and should produce **********)
+(***************** Error: N.y not a defined object *******************)
+\end{coq_eval}
 \begin{coq_example}
 Module N  :  SIG with Definition T := nat  :=  M.
 Print N.T.
@@ -260,7 +265,7 @@ Now let us create a functor, i.e. a parametric module
 Module Two (X Y: SIG).
 \end{coq_example}
 \begin{coq_example*}
-  Definition T := X.T * Y.T.
+  Definition T := (X.T * Y.T)%type.
   Definition x := (X.x, Y.x).
 \end{coq_example*}
 \begin{coq_example}
-- 
cgit v1.2.3