From e35fd10c4ef3c257e91156e07e65234e81672036 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 26 Sep 2003 09:01:01 +0000
Subject: passage V8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8343 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Polynom.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'doc/Polynom.tex')

diff --git a/doc/Polynom.tex b/doc/Polynom.tex
index 2194c3795..d8d16b18a 100644
--- a/doc/Polynom.tex
+++ b/doc/Polynom.tex
@@ -407,17 +407,17 @@ terms generated by rewriting were too big for \Coq's type-checker.
 Let us see why:
 
 \begin{coq_eval}
-Require ZArith.
+Require Import ZArith.
 \end{coq_eval}
 \begin{coq_example}
-Goal (x,y,z:Z)`x + 3 + y + y*z = x + 3 + y + z*y`.
+Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y.
 \end{coq_example}
 \begin{coq_example*}
-Intros; Rewrite (Zmult_sym y z); Reflexivity. 
+intros; rewrite (Zmult_comm y z); reflexivity.
 Save toto.
 \end{coq_example*}
 \begin{coq_example}
-Print toto.
+Print  toto.
 \end{coq_example}
 
 At each step of rewriting, the whole context is duplicated in the proof
-- 
cgit v1.2.3