aboutsummaryrefslogtreecommitdiff
path: root/doc/Omega.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/Omega.tex')
-rwxr-xr-xdoc/Omega.tex3
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{}