diff options
Diffstat (limited to 'doc/refman/Polynom.tex')
| -rw-r--r-- | doc/refman/Polynom.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index 3898bf4c4..664c0d3ff 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -927,7 +927,7 @@ Open Scope Z_scope. 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_comm y z); reflexivity. +intros; rewrite (Z.mul_comm y z); reflexivity. Save toto. \end{coq_example*} \begin{coq_example} |