Move stuff about positive into a distinct PArith subdir

 Beware! after this, a ./configure must be done. It might also
 be a good idea to chase any phantom .vo remaining after a make clean

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7

21 files changed, 71 insertions, 33 deletions

diff --git a/Makefile.common b/Makefile.common
index 77e4d59f2..26484fcdd 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -260,6 +260,7 @@ STRUCTURESVO:=$(call cat_vo_itarget, theories/Structures)
 ARITHVO:=$(call cat_vo_itarget, theories/Arith)
 SORTINGVO:=$(call cat_vo_itarget, theories/Sorting)
 BOOLVO:=$(call cat_vo_itarget, theories/Bool)
+PARITHVO:=$(call cat_vo_itarget, theories/PArith)
 NARITHVO:=$(call cat_vo_itarget, theories/NArith)
 ZARITHVO:=$(call cat_vo_itarget, theories/ZArith)
 QARITHVO:=$(call cat_vo_itarget, theories/QArith)
@@ -278,7 +279,7 @@ CLASSESVO:=$(call cat_vo_itarget, theories/Classes)
 PROGRAMVO:=$(call cat_vo_itarget, theories/Program)
 
 THEORIESVO:=\
-  $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
+  $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
   $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(MSETSVO) \
   $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
   $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO)
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 8847d058a..36549b7a0 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) \\
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index a4feb012b..4f208c7da 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -130,22 +130,31 @@ through the <tt>Require Import</tt> command.</p>
     theories/Arith/Factorial.v
     theories/Arith/Wf_nat.v
   </dd>
-    
-  <dt> <b>NArith</b>:
+
+  <dt> <b>PArith</b>:
     Binary positive integers
   </dt>
+  <dd>
+    theories/PArith/BinPos.v
+    theories/PArith/Pnat.v
+    theories/PArith/POrderedType.v
+    theories/PArith/Pminmax.v
+    theories/PArith/Psqrt.v
+    (theories/PArith/PArith.v)
+  </dd>
+
+  <dt> <b>NArith</b>:
+    Binary natural numbers
+  </dt>
   <dd> 
-    theories/NArith/BinPos.v
     theories/NArith/BinNat.v
-    (theories/NArith/NArith.v)
-    theories/NArith/Pnat.v
     theories/NArith/Nnat.v
     theories/NArith/Ndigits.v
     theories/NArith/Ndist.v
     theories/NArith/Ndec.v
     theories/NArith/Ndiv_def.v
-    theories/NArith/POrderedType.v
-    theories/NArith/Pminmax.v
+    theories/NArith/Nsqrt_def.v
+    (theories/NArith/NArith.v)
   </dd>
 
   <dt> <b>ZArith</b>:
@@ -169,7 +178,8 @@ through the <tt>Require Import</tt> command.</p>
     theories/ZArith/Zhints.v
     (theories/ZArith/ZArith_base.v)
     theories/ZArith/Zcomplements.v
-    theories/ZArith/Zsqrt.v
+    theories/ZArith/Zsqrt_def.v
+    theories/ZArith/Zsqrt_compat.v
     theories/ZArith/Zpow_def.v
     theories/ZArith/Zpower.v
     theories/ZArith/Zdiv.v
@@ -226,6 +236,8 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/NatInt/NZOrder.v
     theories/Numbers/NatInt/NZDomain.v
     theories/Numbers/NatInt/NZProperties.v
+    theories/Numbers/NatInt/NZPow.v
+    theories/Numbers/NatInt/NZSqrt.v
     </dd>
     </dt>
 
@@ -265,8 +277,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Natural/Abstract/NStrongRec.v
     theories/Numbers/Natural/Abstract/NSub.v
     theories/Numbers/Natural/Abstract/NDiv.v
+    theories/Numbers/Natural/Abstract/NMaxMin.v
+    theories/Numbers/Natural/Abstract/NParity.v
+    theories/Numbers/Natural/Abstract/NPow.v
+    theories/Numbers/Natural/Abstract/NSqrt.v
     theories/Numbers/Natural/Abstract/NProperties.v
-    theories/Numbers/Natural/Abstract/NMinMax.v
     theories/Numbers/Natural/Binary/NBinary.v
     theories/Numbers/Natural/Peano/NPeano.v
     theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -288,12 +303,14 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Integer/Abstract/ZLt.v
     theories/Numbers/Integer/Abstract/ZMul.v
     theories/Numbers/Integer/Abstract/ZMulOrder.v
+    theories/Numbers/Integer/Abstract/ZSgnAbs.v
+    theories/Numbers/Integer/Abstract/ZMaxMin.v
+    theories/Numbers/Integer/Abstract/ZParity.v
+    theories/Numbers/Integer/Abstract/ZPow.v
+    theories/Numbers/Integer/Abstract/ZProperties.v
     theories/Numbers/Integer/Abstract/ZDivEucl.v
     theories/Numbers/Integer/Abstract/ZDivFloor.v
     theories/Numbers/Integer/Abstract/ZDivTrunc.v
-    theories/Numbers/Integer/Abstract/ZProperties.v
-    theories/Numbers/Integer/Abstract/ZSgnAbs.v
-    theories/Numbers/Integer/Abstract/ZMinMax.v
     theories/Numbers/Integer/Binary/ZBinary.v
     theories/Numbers/Integer/NatPairs/ZNatPairs.v
     theories/Numbers/Integer/SpecViaZ/ZSig.v
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
index 39cedbec4..c071c4a2e 100755
--- a/doc/stdlib/make-library-files
+++ b/doc/stdlib/make-library-files
@@ -10,7 +10,7 @@
 # En supposant que make fait son boulot, ca fait un tri topologique du
 # graphe des dépendances
 
-LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers"
+LIBDIRS="Arith PArith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers"
 
 rm -f library.files.ls.tmp
 (cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index c8782e93b..8e496fdd2 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -7,7 +7,7 @@ FILE=$1
 cp -f $FILE.template tmp
 echo -n Building file index-list.prehtml ...
 
-LIBDIRS="Init Logic Structures Bool Arith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" 
+LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings"
 
 for k in $LIBDIRS; do
     i=theories/$k
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index bb555148f..d6ed355c9 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -91,10 +91,12 @@ let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
 let arith_dir = ["Coq";"Arith"]
 let arith_modules = [arith_dir]
 
+let parith_dir = ["Coq";"PArith"]
+
 let narith_dir = ["Coq";"NArith"]
 
 let zarith_dir = ["Coq";"ZArith"]
-let zarith_base_modules = [narith_dir;zarith_dir]
+let zarith_base_modules = [parith_dir;narith_dir;zarith_dir]
 
 let init_dir = ["Coq";"Init"]
 let init_modules = [
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 5070f89ed..b235b5821 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -189,9 +189,9 @@ let z0 = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z0")
 let zpos = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Zpos")
 let zneg = lazy(gen_constant "CC" ["ZArith";"BinInt"] "Zneg")
 
-let pxI = lazy(gen_constant "CC" ["NArith";"BinPos"] "xI")
-let pxO = lazy(gen_constant "CC" ["NArith";"BinPos"] "xO")
-let pxH = lazy(gen_constant "CC" ["NArith";"BinPos"] "xH")
+let pxI = lazy(gen_constant "CC" ["PArith";"BinPos"] "xI")
+let pxO = lazy(gen_constant "CC" ["PArith";"BinPos"] "xO")
+let pxH = lazy(gen_constant "CC" ["PArith";"BinPos"] "xH")
 
 let nN0 = lazy (gen_constant "CC" ["NArith";"BinNat"] "N0")
 let nNpos = lazy(gen_constant "CC" ["NArith";"BinNat"] "Npos")
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index cd4a7d3b0..a520ce2d4 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -36,7 +36,7 @@ let l_true_equals_true =
         [|data_constant "bool";data_constant "true"|]))
 
 let pos_constant =
-  Coqlib.gen_constant "refl_tauto" ["NArith";"BinPos"]
+  Coqlib.gen_constant "refl_tauto" ["PArith";"BinPos"]
 
 let l_xI = lazy (pos_constant "xI")
 let l_xO = lazy (pos_constant "xO")
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 15d11eca2..fb8de1f92 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -23,7 +23,7 @@ exception Non_closed_number
 open Libnames
 open Rawterm
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let positive_module = ["Coq";"NArith";"BinPos"]
+let positive_module = ["Coq";"PArith";"BinPos"]
 let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
 
 let positive_path = make_path positive_module "positive"
diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex
index 83eed970e..bf39bc36c 100644
--- a/theories/NArith/intro.tex
+++ b/theories/NArith/intro.tex
@@ -1,4 +1,4 @@
-\section{Binary positive and non negative integers : NArith}\label{NArith}
+\section{Binary natural numbers : NArith}\label{NArith}
 
 Here are defined various arithmetical notions and their properties,
 similar to those of {\tt Arith}.
diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget
index 0caf0b249..1797b25e4 100644
--- a/theories/NArith/vo.itarget
+++ b/theories/NArith/vo.itarget
@@ -1,13 +1,8 @@
 BinNat.vo
-BinPos.vo
 NArith.vo
 Ndec.vo
 Ndigits.vo
 Ndist.vo
 Nnat.vo
 Ndiv_def.vo
-Pnat.vo
-POrderedType.vo
-Pminmax.vo
-Psqrt.vo
 Nsqrt_def.vo
diff --git a/theories/NArith/BinPos.v b/theories/PArith/BinPos.v
index d334d42e9..663233c57 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1253,8 +1253,3 @@ Proof.
   intros; generalize (Pcompare_Gt_Lt _ _ H); auto.
   intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto.
 Qed.
-
-
-
-
-
diff --git a/theories/PArith/PArith.v b/theories/PArith/PArith.v
new file mode 100644
index 000000000..f453af386
--- /dev/null
+++ b/theories/PArith/PArith.v
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Library for positive natural numbers *)
+
+Require Export BinPos.
+Require Export Pnat.
+Require Export Pminmax.
+Require Export Psqrt.
+Require Export POrderedType.
diff --git a/theories/NArith/POrderedType.v b/theories/PArith/POrderedType.v
index 1c4cde6f5..1c4cde6f5 100644
--- a/theories/NArith/POrderedType.v
+++ b/theories/PArith/POrderedType.v
diff --git a/theories/NArith/Pminmax.v b/theories/PArith/Pminmax.v
index 2f753a4c9..2f753a4c9 100644
--- a/theories/NArith/Pminmax.v
+++ b/theories/PArith/Pminmax.v
diff --git a/theories/NArith/Pnat.v b/theories/PArith/Pnat.v
index 715c4484d..715c4484d 100644
--- a/theories/NArith/Pnat.v
+++ b/theories/PArith/Pnat.v
diff --git a/theories/NArith/Psqrt.v b/theories/PArith/Psqrt.v
index 1d85f14a2..1d85f14a2 100644
--- a/theories/NArith/Psqrt.v
+++ b/theories/PArith/Psqrt.v
diff --git a/theories/PArith/intro.tex b/theories/PArith/intro.tex
new file mode 100644
index 000000000..ffce881ed
--- /dev/null
+++ b/theories/PArith/intro.tex
@@ -0,0 +1,4 @@
+\section{Binary positive integers : PArith}\label{PArith}
+
+Here are defined various arithmetical notions and their properties,
+similar to those of {\tt Arith}.
diff --git a/theories/PArith/vo.itarget b/theories/PArith/vo.itarget
new file mode 100644
index 000000000..e9139da8a
--- /dev/null
+++ b/theories/PArith/vo.itarget
@@ -0,0 +1,6 @@
+BinPos.vo
+Pnat.vo
+POrderedType.vo
+Pminmax.vo
+Psqrt.vo
+PArith.vo
\ No newline at end of file
diff --git a/theories/theories.itarget b/theories/theories.itarget
index afc3554b1..7cc4e09a9 100644
--- a/theories/theories.itarget
+++ b/theories/theories.itarget
@@ -7,6 +7,7 @@ Structures/vo.otarget
 Init/vo.otarget
 Lists/vo.otarget
 Logic/vo.otarget
+PArith/vo.otarget
 NArith/vo.otarget
 Numbers/vo.otarget
 Program/vo.otarget
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 26a5cb36f..a62510b68 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -77,6 +77,7 @@ let theories_dirs_map = [
     "theories/Relations", "Relations" ;
     "theories/Numbers", "Numbers" ;
     "theories/QArith", "QArith" ;
+    "theories/PArith", "PArith" ;
     "theories/NArith", "NArith" ;
     "theories/ZArith", "ZArith" ;
     "theories/Arith", "Arith" ;