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 ++-
 doc/RefMan.txt           | 2 +-
 doc/Reference-Manual.tex | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'doc')

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{}
diff --git a/doc/RefMan.txt b/doc/RefMan.txt
index 3c3d88ba8e..75a762758f 100644
--- a/doc/RefMan.txt
+++ b/doc/RefMan.txt
@@ -42,7 +42,7 @@ MANUEL DE REFERENCE
 \include{Cases.v}%						CP
 \include{Coercion.v}%						HH
 %%SUPPRIME \include{Natural.v}%
-\include{Omega.v}%						JCF
+\include{Omega.v}%						JCF - fait
 %%Nouvelle version ROmega					Pierre Cregut
 %%SUPPRIME \include{Program.v}%
 %% A SUPPRIMER
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index c32d053682..229fb4524b 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -18,7 +18,7 @@
 \fi
 
 
-%\includeonly{RefMan-cic.v,RefMan-ext.v,RefMan-modr}
+%\includeonly{RefMan-tac.v,RefMan-tacex.v}
 
 \input{./version.tex}
 \input{./macros.tex}% extension .tex pour htmlgen
-- 
cgit v1.2.3