aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/RefMan-lib.tex
diff options
context:
space:
mode:
authorGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-19 13:30:17 +0000
committerGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-19 13:30:17 +0000
commitc18e2a18fc080ec982f74a6113e9af6c702ab2d1 (patch)
treedb41a03445890759685f9ae949a05856bc503e7c /doc/RefMan-lib.tex
parent1d6689788d3ffe952cfe9b51b338d30c5aeeda14 (diff)
Changement de Zarith en ZArith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8194 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan-lib.tex')
-rwxr-xr-xdoc/RefMan-lib.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 2ce2e34e8..d0c16e3c2 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). \\