diff options
Diffstat (limited to 'doc/refman/RefMan-lib.tex')
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 2c8abc88..31c6fef4 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -809,7 +809,8 @@ subdirectories: \begin{tabular}{lp{12cm}} {\bf Logic} & Classical logic and dependent equality \\ {\bf Arith} & Basic Peano arithmetic \\ - {\bf NArith} & Basic positive integer arithmetic \\ + {\bf PArith} & Basic positive integer arithmetic \\ + {\bf NArith} & Basic binary natural number arithmetic \\ {\bf ZArith} & Basic relative integer arithmetic \\ {\bf Numbers} & Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2$^{31}$ binary words) \\ {\bf Bool} & Booleans (basic functions and results) \\ @@ -996,7 +997,7 @@ Abort. \end{coq_eval} \item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits -corresponding conjonctions. +corresponding conjunctions. \tacindex{split\_Rabs} \begin{coq_example*} @@ -1094,8 +1095,6 @@ description, etc.) and the possibility to download them one by one. You will also find informations on how to submit a new contribution. -% $Id: RefMan-lib.tex 13091 2010-06-08 13:56:19Z herbelin $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" |