diff options
Diffstat (limited to 'doc/Polynom.tex')
| -rw-r--r-- | doc/Polynom.tex | 8 |
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 |