From 48aff2bc219295950c032ba09b748f0690f5a2bc Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 6 Apr 2001 12:18:05 +0000
Subject: mise � jour V7

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

diff --git a/doc/Omega.tex b/doc/Omega.tex
index 286c151c46..708e1f089c 100755
--- a/doc/Omega.tex
+++ b/doc/Omega.tex
@@ -50,7 +50,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!+, -, *, Zs!, and constants.
 \end{quote}
 
 All expressions of type \verb=nat= or \verb=Z= not built on these
@@ -142,7 +142,7 @@ Goal (z:Z)`z>0` -> `2*z + 1 > z`.
 Intro; Omega.
 \end{coq_example}
 
-Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
+% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
 
 \asection{Technical data}
 \label{technical}
@@ -209,7 +209,7 @@ decision procedure is only partial.
 
 \item Much too slow.
 
-\item Certainely plenty other bugs !! You can report them to
+\item Certainely other bugs! You can report them to
 
 \begin{quote}
   \verb=Pierre.Cregut@cnet.francetelecom.fr= 
-- 
cgit v1.2.3