maj Omega

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

1 files changed, 2 insertions, 1 deletions

diff --git a/doc/Omega.tex b/doc/Omega.tex
index 14bafc2a08..69764336d2 100755
--- a/doc/Omega.tex
+++ b/doc/Omega.tex
@@ -51,7 +51,7 @@ on atomic formulas. Atomic formulas are built from the predicates
 and in expressions of type \verb=Z=, {\tt Omega}~recognizes 
 
 \begin{quote}
-\verb!+, -, *, Zs!, and constants.
+\verb!+, -, *, Zsucc!, and constants.
 \end{quote}
 
 All expressions of type \verb=nat= or \verb=Z= not built on these
@@ -124,6 +124,7 @@ loaded by
 
 \begin{coq_example*}
 Require Import Omega.
+Open Scope Z_scope.
 \end{coq_example*}
 
 \example{}