diff options
author | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 13:30:17 +0000 |
---|---|---|
committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 13:30:17 +0000 |
commit | c18e2a18fc080ec982f74a6113e9af6c702ab2d1 (patch) | |
tree | db41a03445890759685f9ae949a05856bc503e7c | |
parent | 1d6689788d3ffe952cfe9b51b338d30c5aeeda14 (diff) |
Changement de Zarith en ZArith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8194 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-x | doc/Library.tex | 4 | ||||
-rwxr-xr-x | doc/RefMan-lib.tex | 4 | ||||
-rw-r--r-- | doc/RefMan-tac.tex | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/doc/Library.tex b/doc/Library.tex index 321c4057e..c66b6e1cf 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 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). \\ diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 8cfecf594..44f31379b 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. |