passage V8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8343 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

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