From c18e2a18fc080ec982f74a6113e9af6c702ab2d1 Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 19 Apr 2001 13:30:17 +0000
Subject: Changement de Zarith en ZArith

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8194 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Library.tex    | 4 ++--
 doc/RefMan-lib.tex | 4 ++--
 doc/RefMan-tac.tex | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/doc/Library.tex b/doc/Library.tex
index 321c4057ec..c66b6e1cf1 100755
--- a/doc/Library.tex
+++ b/doc/Library.tex
@@ -31,10 +31,10 @@ The standard library is composed of the following subdirectories:
   {\bf Logic}   & Classical logic and dependent equality \\
   {\bf Bool}    & Booleans (basic functions and results) \\
   {\bf Arith}   & Basic Peano arithmetic \\
-  {\bf Zarith}  & Basic integer arithmetic \\
+  {\bf ZArith}  & Basic integer arithmetic \\
   {\bf Reals}   & Axiomatization of Real Numbers (classical, basic functions 
                   and results, integer part and fractional part,
-                  requires the \textbf{Zarith} library).\\
+                  requires the \textbf{ZArith} library).\\
   {\bf Lists}   & Monomorphic and polymorphic lists (basic functions and
                   results), Streams (infinite sequences defined 
                   with co-inductive types) \\
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 2ce2e34e89..d0c16e3c2c 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -790,7 +790,7 @@ subdirectories:
 \begin{tabular}{lp{12cm}}
   {\bf Logic}   & Classical logic and dependent equality \\
   {\bf Arith}   & Basic Peano arithmetic \\
-  {\bf Zarith}  & Basic integer arithmetic \\
+  {\bf ZArith}  & Basic integer arithmetic \\
   {\bf Bool}    &  Booleans (basic functions and results) \\
   {\bf Lists}   & Monomorphic and polymorphic lists (basic functions and
             results), Streams (infinite sequences defined with co-inductive
@@ -801,7 +801,7 @@ subdirectories:
   structure of map (trees indexed by binary integers).\\
  {\bf Reals}   & Axiomatization of Real Numbers (classical, basic functions 
                  and results, integer part and fractional part,
-                 requires the \textbf{Zarith} library).\\
+                 requires the \textbf{ZArith} library).\\
  {\bf Relations} & Relations (definitions and basic results). \\
  {\bf Wellfounded} & Well-founded relations (basic results). \\
 
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 8cfecf5948..44f31379b1 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1626,7 +1626,7 @@ Reset Initial.
 \end{coq_eval}
 
 You can have a look at the files \texttt{Ring.v},
-\texttt{ArithRing.v}, \texttt{ZarithRing.v} to see examples of the
+\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the
 \texttt{Add Ring} command.
 
 \SeeAlso Chapter~\ref{Ring} for more detailed explanations about this tactic.
-- 
cgit v1.2.3