diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
| commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
| tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /doc/refman/RefMan-lib.tex | |
| parent | 300293c119981054c95182a90c829058530a6b6f (diff) | |
Imported Upstream version 8.4~betaupstream/8.4_beta
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" |