From d418004b79b5f95898eafa0b5376d5afc30cd699 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 16 Dec 2003 15:23:07 +0000
Subject: maj Omega

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8400 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Omega.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/Omega.tex')

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{}
-- 
cgit v1.2.3