Integration of theories/Ints into theories/Numbers, part 1: moving files

For the moment, the Ints files are simply moved into directories in
theories/Numbers with meaningful names. No filenames changed, apart
from: 
 Zaux.v -> theories/Numbers/BigNumPrelude.v 
 MemoFn.v -> theories/Lists/StreamMemo.v

More to come...



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

31 files changed, 315 insertions, 358 deletions

diff --git a/Makefile.build b/Makefile.build
index 0d57feae0..35786edf8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -477,7 +477,6 @@ fsets: $(FSETSVO)
 allfsets: $(ALLFSETS)
 relations: $(RELATIONSVO)
 wellfounded: $(WELLFOUNDEDVO)
-ints: $(INTSVO)
 # reals
 reals: $(REALSVO)
 allreals: $(ALLREALS)
diff --git a/Makefile.common b/Makefile.common
index 315ed912a..a01110cd1 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -359,7 +359,7 @@ INTERFACE:=\
 
 INTERFACECMX:=$(INTERFACE:.cmo=.cmx)
 
-PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité...
+PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité...
 PARSERREQUIRESCMX:=$(LINKCMX)
 
 ifeq ($(BEST),opt)
@@ -487,329 +487,267 @@ PRINTERSCMO:=\
 
 ## Theories
 
-INITVO:=\
- theories/Init/Notations.vo \
- theories/Init/Datatypes.vo         theories/Init/Peano.vo     \
- theories/Init/Logic.vo             theories/Init/Specif.vo    \
- theories/Init/Logic_Type.vo        theories/Init/Wf.vo      \
- theories/Init/Tactics.vo           theories/Init/Prelude.vo
-
-LOGICVO:=\
- theories/Logic/Hurkens.vo            theories/Logic/ProofIrrelevance.vo\
- theories/Logic/Classical.vo          theories/Logic/Classical_Type.vo \
- theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo          \
- theories/Logic/Classical_Prop.vo     theories/Logic/Classical_Pred_Type.vo \
- theories/Logic/ClassicalFacts.vo     theories/Logic/ChoiceFacts.vo \
- theories/Logic/Berardi.vo            theories/Logic/Eqdep_dec.vo \
- theories/Logic/Decidable.vo          theories/Logic/JMeq.vo \
- theories/Logic/ClassicalChoice.vo    theories/Logic/ClassicalDescription.vo \
- theories/Logic/RelationalChoice.vo   theories/Logic/Diaconescu.vo \
- theories/Logic/EqdepFacts.vo         theories/Logic/ProofIrrelevanceFacts.vo \
- theories/Logic/ClassicalEpsilon.vo   theories/Logic/ClassicalUniqueChoice.vo \
- theories/Logic/DecidableType.vo      theories/Logic/DecidableTypeEx.vo \
- theories/Logic/Epsilon.vo            theories/Logic/ConstructiveEpsilon.vo \
- theories/Logic/Description.vo        theories/Logic/IndefiniteDescription.vo \
- theories/Logic/SetIsType.vo
-
-ARITHVO:=\
- theories/Arith/Arith.vo        theories/Arith/Gt.vo          \
- theories/Arith/Between.vo      theories/Arith/Le.vo          \
- theories/Arith/Compare.vo      theories/Arith/Lt.vo          \
- theories/Arith/Compare_dec.vo  theories/Arith/Min.vo         \
- theories/Arith/Div2.vo         theories/Arith/Minus.vo       \
- theories/Arith/Mult.vo         theories/Arith/Even.vo        \
- theories/Arith/EqNat.vo        theories/Arith/Peano_dec.vo   \
- theories/Arith/Euclid.vo       theories/Arith/Plus.vo        \
- theories/Arith/Wf_nat.vo  	theories/Arith/Max.vo	      \
- theories/Arith/Bool_nat.vo	theories/Arith/Factorial.vo   \
- theories/Arith/Arith_base.vo 
-
-SORTINGVO:=\
- theories/Sorting/Heap.vo	theories/Sorting/Permutation.vo \
- theories/Sorting/Sorting.vo	theories/Sorting/PermutSetoid.vo \
- theories/Sorting/PermutEq.vo
-
-BOOLVO:=\
- theories/Bool/Bool.vo  	theories/Bool/IfProp.vo \
- theories/Bool/Zerob.vo 	theories/Bool/DecBool.vo \
- theories/Bool/Sumbool.vo 	theories/Bool/BoolEq.vo \
- theories/Bool/Bvector.vo
-
-NARITHVO:=\
- theories/NArith/BinPos.vo	theories/NArith/Pnat.vo \
- theories/NArith/BinNat.vo	theories/NArith/NArith.vo \
- theories/NArith/Nnat.vo	theories/NArith/Ndigits.vo \
- theories/NArith/Ndec.vo	theories/NArith/Ndist.vo 
-
-ZARITHVO:=\
- theories/ZArith/BinInt.vo      theories/ZArith/Wf_Z.vo \
- theories/ZArith/ZArith.vo      theories/ZArith/ZArith_dec.vo \
- theories/ZArith/auxiliary.vo   theories/ZArith/Zmisc.vo \
- theories/ZArith/Zcompare.vo    theories/ZArith/Znat.vo \
- theories/ZArith/Zorder.vo      theories/ZArith/Zabs.vo \
- theories/ZArith/Zmin.vo        theories/ZArith/Zmax.vo \
- theories/ZArith/Zminmax.vo     theories/ZArith/Zeven.vo \
- theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
- theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo \
- theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo \
- theories/ZArith/Zwf.vo		theories/ZArith/ZArith_base.vo \
- theories/ZArith/Zbool.vo	theories/ZArith/Zbinary.vo \
- theories/ZArith/Znumtheory.vo  theories/ZArith/Int.vo \
- theories/ZArith/Zpow_def.vo	theories/ZArith/Zpow_facts.vo \
- theories/ZArith/ZOdiv_def.vo   theories/ZArith/ZOdiv.vo
-
-INTSVO:=\
- theories/Ints/Zaux.vo \
- theories/Ints/Basic_type.vo theories/Ints/Int31.vo \
- theories/Ints/num/GenBase.vo theories/Ints/num/ZnZ.vo \
- theories/Ints/num/GenAdd.vo theories/Ints/num/GenSub.vo \
- theories/Ints/num/GenMul.vo theories/Ints/num/GenDivn1.vo \
- theories/Ints/num/GenDiv.vo theories/Ints/num/GenSqrt.vo \
- theories/Ints/num/GenLift.vo theories/Ints/num/Zn2Z.vo\
- theories/Ints/num/Nbasic.vo theories/Ints/num/NMake.vo \
- theories/Ints/num/MemoFn.vo \
- theories/Ints/BigN.vo theories/Ints/num/ZMake.vo \
- theories/Ints/BigZ.vo theories/Ints/num/BigQ.vo \
- theories/Ints/num/QMake_base.vo theories/Ints/num/QpMake.vo \
- theories/Ints/num/QvMake.vo theories/Ints/num/Q0Make.vo \
- theories/Ints/num/QifMake.vo  theories/Ints/num/QbiMake.vo 
-# spiwack : should use the genN.ml to create NMake eventually
-# arnaud : see above
-
-QARITHVO:=\
- theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \
- theories/QArith/Qring.vo       theories/QArith/Qreals.vo \
- theories/QArith/QArith.vo	theories/QArith/Qcanon.vo \
- theories/QArith/Qfield.vo	theories/QArith/Qpower.vo \
- theories/QArith/Qabs.vo        theories/QArith/Qround.vo
-
-LISTSVO:=\
- theories/Lists/MonoList.vo \
- theories/Lists/ListSet.vo   	theories/Lists/Streams.vo \
- theories/Lists/TheoryList.vo   theories/Lists/List.vo \
- theories/Lists/SetoidList.vo   theories/Lists/ListTactics.vo
-
-STRINGSVO:=\
- theories/Strings/Ascii.vo      theories/Strings/String.vo
-
-SETSVO:=\
- theories/Sets/Classical_sets.vo    theories/Sets/Permut.vo \
- theories/Sets/Constructive_sets.vo theories/Sets/Powerset.vo \
- theories/Sets/Cpo.vo               theories/Sets/Powerset_Classical_facts.vo \
- theories/Sets/Ensembles.vo         theories/Sets/Powerset_facts.vo \
- theories/Sets/Finite_sets.vo       theories/Sets/Relations_1.vo \
- theories/Sets/Finite_sets_facts.vo theories/Sets/Relations_1_facts.vo \
- theories/Sets/Image.vo             theories/Sets/Relations_2.vo \
- theories/Sets/Infinite_sets.vo     theories/Sets/Relations_2_facts.vo \
- theories/Sets/Integers.vo          theories/Sets/Relations_3.vo \
- theories/Sets/Multiset.vo          theories/Sets/Relations_3_facts.vo \
- theories/Sets/Partial_Order.vo     theories/Sets/Uniset.vo
-
-FSETSBASEVO:=\
- theories/FSets/OrderedType.vo \
- theories/FSets/OrderedTypeEx.vo     theories/FSets/OrderedTypeAlt.vo \
- theories/FSets/FSetInterface.vo     theories/FSets/FSetList.vo \
- theories/FSets/FSetBridge.vo        theories/FSets/FSetFacts.vo \
- theories/FSets/FSetProperties.vo    theories/FSets/FSetEqProperties.vo \
- theories/FSets/FSets.vo             theories/FSets/FSetWeakList.vo \
- theories/FSets/FMapInterface.vo     theories/FSets/FMapList.vo \
- theories/FSets/FMaps.vo             theories/FSets/FMapFacts.vo \
- theories/FSets/FMapWeakList.vo      theories/FSets/FMapPositive.vo \
- theories/FSets/FSetToFiniteSet.vo   theories/FSets/FSetDecide.vo \
- theories/FSets/FSetAVL.vo           
+INITVO:=$(addprefix theories/Init/, \
+ Notations.vo	Datatypes.vo	Peano.vo	Logic.vo	\
+ Specif.vo	Logic_Type.vo  	Wf.vo		Tactics.vo	\
+ Prelude.vo )
+
+LOGICVO:=$(addprefix theories/Logic/, \
+ Hurkens.vo               ProofIrrelevance.vo      Classical.vo 	\
+ Classical_Type.vo        Classical_Pred_Set.vo    Eqdep.vo     	\
+ Classical_Prop.vo        Classical_Pred_Type.vo   ClassicalFacts.vo 	\
+ ChoiceFacts.vo           Berardi.vo               Eqdep_dec.vo 	\
+ Decidable.vo             JMeq.vo                  ClassicalChoice.vo 	\
+ ClassicalDescription.vo  RelationalChoice.vo      Diaconescu.vo 	\
+ EqdepFacts.vo            ProofIrrelevanceFacts.vo ClassicalEpsilon.vo 	\
+ ClassicalUniqueChoice.vo DecidableType.vo         DecidableTypeEx.vo 	\
+ Epsilon.vo               ConstructiveEpsilon.vo   Description.vo 	\
+ IndefiniteDescription.vo SetIsType.vo )
+
+ARITHVO:=$(addprefix theories/Arith/, \
+ Arith.vo	Gt.vo          	Between.vo	Le.vo          \
+ Compare.vo	Lt.vo          	Compare_dec.vo	Min.vo         \
+ Div2.vo	Minus.vo       	Mult.vo		Even.vo        \
+ EqNat.vo	Peano_dec.vo   	Euclid.vo	Plus.vo        \
+ Wf_nat.vo  	Max.vo		Factorial.vo	Arith_base.vo  )
+
+SORTINGVO:=$(addprefix theories/Sorting/, \
+ Heap.vo 	Permutation.vo	Sorting.vo 	PermutSetoid.vo \
+ PermutEq.vo )
+
+BOOLVO:=$(addprefix theories/Bool/, \
+ Bool.vo  	IfProp.vo    	Zerob.vo 	DecBool.vo 	\
+ Sumbool.vo 	BoolEq.vo    	Bvector.vo )
+
+NARITHVO:=$(addprefix theories/NArith/, \
+ BinPos.vo	Pnat.vo      	BinNat.vo   	NArith.vo 	\
+ Nnat.vo	Ndigits.vo   	Ndec.vo	 	Ndist.vo 	)
+
+ZARITHVO:=$(addprefix theories/ZArith/, \
+ BinInt.vo      Wf_Z.vo 	ZArith.vo      	ZArith_dec.vo 	\
+ auxiliary.vo   Zmisc.vo 	Zcompare.vo    	Znat.vo 	\
+ Zorder.vo      Zabs.vo 	Zmin.vo        	Zmax.vo 	\
+ Zminmax.vo     Zeven.vo 	Zhints.vo	Zlogarithm.vo 	\
+ Zpower.vo 	Zcomplements.vo Zdiv.vo		Zsqrt.vo 	\
+ Zwf.vo		ZArith_base.vo 	Zbool.vo	Zbinary.vo 	\
+ Znumtheory.vo  Int.vo 		Zpow_def.vo	Zpow_facts.vo 	\
+ ZOdiv_def.vo   ZOdiv.vo )
+
+QARITHVO:=$(addprefix theories/QArith/, \
+ QArith_base.vo Qreduction.vo 	Qring.vo	Qreals.vo 	\
+ QArith.vo	Qcanon.vo 	Qfield.vo	Qpower.vo 	\
+ Qabs.vo        Qround.vo )
+
+LISTSVO:=$(addprefix theories/Lists/, \
+ MonoList.vo  	ListSet.vo   	Streams.vo 	StreamMemo.vo  \
+ TheoryList.vo	List.vo 	SetoidList.vo   ListTactics.vo )
+
+STRINGSVO:=$(addprefix theories/Strings/, \
+ Ascii.vo      	String.vo )
+
+SETSVO:=$(addprefix theories/Sets/, \
+ Classical_sets.vo    	Permut.vo \
+ Constructive_sets.vo 	Powerset.vo \
+ Cpo.vo               	Powerset_Classical_facts.vo \
+ Ensembles.vo         	Powerset_facts.vo \
+ Finite_sets.vo       	Relations_1.vo \
+ Finite_sets_facts.vo 	Relations_1_facts.vo \
+ Image.vo             	Relations_2.vo \
+ Infinite_sets.vo     	Relations_2_facts.vo \
+ Integers.vo          	Relations_3.vo \
+ Multiset.vo          	Relations_3_facts.vo \
+ Partial_Order.vo     	Uniset.vo )
+
+FSETSBASEVO:=$(addprefix theories/FSets/, \
+ OrderedType.vo		OrderedTypeEx.vo	OrderedTypeAlt.vo	\
+ FSetInterface.vo	FSetList.vo 		FSetBridge.vo        	\
+ FSetFacts.vo 		FSetProperties.vo	FSetEqProperties.vo 	\
+ FSetWeakList.vo 	FSetAVL.vo           	FSetDecide.vo 		\
+ FSets.vo \
+ FMapInterface.vo       FMapList.vo		FMapFacts.vo 		\
+ FMapWeakList.vo      	FMapPositive.vo		FSetToFiniteSet.vo   	\
+ FMaps.vo )            
 
 FSETS_basic:=
 
-FSETS_all:=\
- theories/FSets/FSetFullAVL.vo \
- theories/FSets/FMapAVL.vo theories/FSets/FMapFullAVL.vo
+FSETS_all:=$(addprefix theories/FSets/, \
+ FSetFullAVL.vo 	FMapAVL.vo 		FMapFullAVL.vo )
 
 FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS))
 
 ALLFSETS:=$(FSETSBASEVO) $(FSETS_all)
 
-RELATIONSVO:=\
- theories/Relations/Newman.vo \
- theories/Relations/Operators_Properties.vo \
- theories/Relations/Relation_Definitions.vo \
- theories/Relations/Relation_Operators.vo \
- theories/Relations/Relations.vo \
- theories/Relations/Rstar.vo
-
-WELLFOUNDEDVO:=\
- theories/Wellfounded/Disjoint_Union.vo \
- theories/Wellfounded/Inclusion.vo \
- theories/Wellfounded/Inverse_Image.vo \
- theories/Wellfounded/Lexicographic_Exponentiation.vo \
- theories/Wellfounded/Transitive_Closure.vo \
- theories/Wellfounded/Union.vo \
- theories/Wellfounded/Wellfounded.vo \
- theories/Wellfounded/Well_Ordering.vo \
- theories/Wellfounded/Lexicographic_Product.vo 
-
-REALSBASEVO:=\
- theories/Reals/Rdefinitions.vo \
- theories/Reals/Raxioms.vo      theories/Reals/RIneq.vo \
- theories/Reals/DiscrR.vo       theories/Reals/Rbase.vo \
- theories/Reals/LegacyRfield.vo theories/Reals/Rpow_def.vo
-
-REALS_basic= 
-
-REALS_all=\
- theories/Reals/R_Ifp.vo \
- theories/Reals/Rbasic_fun.vo   theories/Reals/R_sqr.vo \
- theories/Reals/SplitAbsolu.vo  theories/Reals/SplitRmult.vo \
- theories/Reals/ArithProp.vo    theories/Reals/Rfunctions.vo \
- theories/Reals/Rseries.vo      theories/Reals/SeqProp.vo \
- theories/Reals/Rcomplete.vo    theories/Reals/PartSum.vo \
- theories/Reals/AltSeries.vo    theories/Reals/Binomial.vo \
- theories/Reals/Rsigma.vo       theories/Reals/Rprod.vo \
- theories/Reals/Cauchy_prod.vo  theories/Reals/Alembert.vo \
- theories/Reals/SeqSeries.vo    theories/Reals/Rtrigo_fun.vo \
- theories/Reals/Rtrigo_def.vo   theories/Reals/Rtrigo_alt.vo \
- theories/Reals/Cos_rel.vo      theories/Reals/Cos_plus.vo \
- theories/Reals/Rtrigo.vo       theories/Reals/Rlimit.vo \
- theories/Reals/Rderiv.vo       theories/Reals/RList.vo \
- theories/Reals/Ranalysis1.vo   theories/Reals/Ranalysis2.vo \
- theories/Reals/Ranalysis3.vo   theories/Reals/Rtopology.vo \
- theories/Reals/MVT.vo          theories/Reals/PSeries_reg.vo \
- theories/Reals/Exp_prop.vo     theories/Reals/Rtrigo_reg.vo \
- theories/Reals/Rsqrt_def.vo    theories/Reals/R_sqrt.vo \
- theories/Reals/Rtrigo_calc.vo  theories/Reals/Rgeom.vo \
- theories/Reals/Sqrt_reg.vo     theories/Reals/Ranalysis4.vo \
- theories/Reals/Rpower.vo       theories/Reals/Ranalysis.vo \
- theories/Reals/NewtonInt.vo    theories/Reals/RiemannInt_SF.vo \
- theories/Reals/RiemannInt.vo   theories/Reals/Integration.vo \
- theories/Reals/Rlogic.vo	theories/Reals/Reals.vo
+RELATIONSVO:=$(addprefix theories/Relations/, \
+ Newman.vo 		Operators_Properties.vo	Relation_Definitions.vo \
+ Relation_Operators.vo 	Relations.vo 		Rstar.vo )
+
+WELLFOUNDEDVO:=$(addprefix theories/Wellfounded/, \
+ Disjoint_Union.vo 	Inclusion.vo 	Inverse_Image.vo \
+ Transitive_Closure.vo  Union.vo 	Wellfounded.vo 	 \
+ Well_Ordering.vo 	Lexicographic_Product.vo         \
+ Lexicographic_Exponentiation.vo )
+
+REALSBASEVO:=$(addprefix theories/Reals/, \
+ Rdefinitions.vo Raxioms.vo      RIneq.vo	DiscrR.vo \
+ Rbase.vo 	 LegacyRfield.vo Rpow_def.vo )
+
+REALS_basic:= 
+
+REALS_all:=$(addprefix theories/Reals/, \
+ R_Ifp.vo 	Rbasic_fun.vo	R_sqr.vo	SplitAbsolu.vo	\
+ SplitRmult.vo	ArithProp.vo    Rfunctions.vo	Rseries.vo      \
+ SeqProp.vo 	Rcomplete.vo    PartSum.vo	AltSeries.vo    \
+ Binomial.vo	Rsigma.vo       Rprod.vo	Cauchy_prod.vo  \
+ Alembert.vo	SeqSeries.vo    Rtrigo_fun.vo	Rtrigo_def.vo   \
+ Rtrigo_alt.vo  Cos_rel.vo      Cos_plus.vo	Rtrigo.vo       \
+ Rlimit.vo	Rderiv.vo       RList.vo	Ranalysis1.vo   \
+ Ranalysis2.vo	Ranalysis3.vo   Rtopology.vo	MVT.vo          \
+ PSeries_reg.vo Exp_prop.vo     Rtrigo_reg.vo	Rsqrt_def.vo    \
+ R_sqrt.vo	Rtrigo_calc.vo  Rgeom.vo	Sqrt_reg.vo     \
+ Ranalysis4.vo	Rpower.vo       Ranalysis.vo	NewtonInt.vo    \
+ RiemannInt_SF.vo		RiemannInt.vo   Integration.vo 	\
+ Rlogic.vo	Reals.vo )
 
 REALSVO:=$(REALSBASEVO) $(REALS_$(REALS))
 
 ALLREALS:=$(REALSBASEVO) $(REALS_all)
 
-NUMBERSDIR:=theories/Numbers
-NUMBERSCOMMONVO:=$(NUMBERSDIR)/QRewrite.vo $(NUMBERSDIR)/NumPrelude.vo
-NATINTDIR:=$(NUMBERSDIR)/NatInt
-NATINTVO:=\
-  $(NATINTDIR)/NZAxioms.vo\
-  $(NATINTDIR)/NZBase.vo\
-  $(NATINTDIR)/NZPlus.vo\
-  $(NATINTDIR)/NZTimes.vo\
-  $(NATINTDIR)/NZOrder.vo\
-  $(NATINTDIR)/NZPlusOrder.vo\
-  $(NATINTDIR)/NZTimesOrder.vo
-
-NATURALDIR:=$(NUMBERSDIR)/Natural
-NATABSTRACTDIR:=$(NATURALDIR)/Abstract
-NATURALABSTRACTVO:=\
-  $(NATABSTRACTDIR)/NAxioms.vo\
-  $(NATABSTRACTDIR)/NBase.vo\
-  $(NATABSTRACTDIR)/NPlus.vo\
-  $(NATABSTRACTDIR)/NTimes.vo\
-  $(NATABSTRACTDIR)/NOrder.vo\
-  $(NATABSTRACTDIR)/NPlusOrder.vo\
-  $(NATABSTRACTDIR)/NTimesOrder.vo\
-  $(NATABSTRACTDIR)/NMinus.vo\
-  $(NATABSTRACTDIR)/NIso.vo
-
-NATURALPEANOVO:=$(NATURALDIR)/Peano/NPeano.vo
-
-NATURALBINARYVO:=\
-  $(NATURALDIR)/Binary/NBinDefs.vo\
-  $(NATURALDIR)/Binary/NBinary.vo
-
-NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO)
-
-INTEGERDIR:=$(NUMBERSDIR)/Integer
-INTABSTRACTDIR:=$(INTEGERDIR)/Abstract
-INTEGERABSTRACTVO:=\
-  $(INTABSTRACTDIR)/ZAxioms.vo\
-  $(INTABSTRACTDIR)/ZBase.vo\
-  $(INTABSTRACTDIR)/ZPlus.vo\
-  $(INTABSTRACTDIR)/ZTimes.vo\
-  $(INTABSTRACTDIR)/ZLt.vo\
-  $(INTABSTRACTDIR)/ZPlusOrder.vo\
-  $(INTABSTRACTDIR)/ZTimesOrder.vo
-
-INTEGERBINARYVO:=$(INTEGERDIR)/Binary/ZBinary.vo
-
-INTEGERNATPAIRSVO:=$(INTEGERDIR)/NatPairs/ZNatPairs.vo
-
-INTEGERTREEMODVO:=$(INTEGERDIR)/TreeMod/ZTreeMod.vo
-
-INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) $(INTEGERTREEMODVO)
-
-NUMBERSVO:= $(NUMBERSCOMMONVO) $(NATURALVO) $(INTEGERVO) $(NATINTVO)
-
-SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo
-
-UNICODEVO:= theories/Unicode/Utf8.vo
-
-CLASSESVO:= theories/Classes/Init.vo theories/Classes/RelationClasses.vo theories/Classes/Morphisms.vo \
-	theories/Classes/Morphisms_Prop.vo theories/Classes/Morphisms_Relations.vo \
-	theories/Classes/Functions.vo theories/Classes/Equivalence.vo theories/Classes/SetoidTactics.vo \
-	theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/EquivDec.vo \
-	 theories/Classes/SetoidDec.vo
+NUMBERSCOMMONVO:=$(addprefix theories/Numbers/, \
+ QRewrite.vo	NumPrelude.vo	BigNumPrelude.vo )
+
+CYCLICABSTRACTVO:=$(addprefix theories/Numbers/Cyclic/Abstract/, \
+ ZnZ.vo )
+
+CYCLICINT31VO:=$(addprefix theories/Numbers/Cyclic/Int31/, \
+ Int31.vo )
+
+CYCLICDOUBLECYCLICVO:=$(addprefix theories/Numbers/Cyclic/DoubleCyclic/, \
+ Basic_type.vo	GenBase.vo	GenAdd.vo	GenSub.vo	\
+ GenMul.vo	GenDivn1.vo 	GenDiv.vo	GenSqrt.vo	\
+ GenLift.vo 	Zn2Z.vo )
+
+CYCLICVO:=$(CYCLICABSTRACTVO) $(CYCLICINT31VO) $(CYCLICDOUBLECYCLICVO)
+
+NATINTVO:=$(addprefix theories/Numbers/NatInt/, \
+ NZAxioms.vo	NZBase.vo	NZPlus.vo	NZTimes.vo	\
+ NZOrder.vo 	NZPlusOrder.vo	NZTimesOrder.vo )
+
+NATURALABSTRACTVO:=$(addprefix theories/Numbers/Natural/Abstract/, \
+ NAxioms.vo 	NBase.vo 	NPlus.vo 	NTimes.vo 	\
+ NOrder.vo 	NPlusOrder.vo	NTimesOrder.vo 	NMinus.vo	\
+ NIso.vo )
+
+NATURALPEANOVO:=$(addprefix theories/Numbers/Natural/Peano/, \
+ NPeano.vo )
+
+NATURALBINARYVO:=$(addprefix theories/Numbers/Natural/Binary/, \
+ NBinDefs.vo 	NBinary.vo )
+
+NATURALBIGNVO:=$(addprefix theories/Numbers/Natural/BigN/, \
+ Nbasic.vo 	NMake.vo 	BigN.vo )
+
+NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) $(NATURALBIGNVO)
+
+INTEGERABSTRACTVO:=$(addprefix theories/Numbers/Integer/Abstract/, \
+ ZAxioms.vo 	ZBase.vo 	ZPlus.vo 	ZTimes.vo 	\
+ ZLt.vo 	ZPlusOrder.vo 	ZTimesOrder.vo )
+
+INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \
+ ZBinary.vo )
+
+INTEGERNATPAIRSVO:=$(addprefix theories/Numbers/Integer/NatPairs/, \
+ ZNatPairs.vo )
+
+INTEGERTREEMODVO:=$(addprefix theories/Numbers/Integer/TreeMod/, \
+ ZTreeMod.vo )
+
+INTEGERBIGZVO:=$(addprefix theories/Numbers/Integer/BigZ/, \
+ ZMake.vo 	BigZ.vo )
+
+INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) \
+ $(INTEGERTREEMODVO) $(INTEGERBIGZVO)
+
+RATIONALBIGQVO:=$(addprefix theories/Numbers/Rational/BigQ/, \
+ QMake_base.vo	QpMake.vo	QvMake.vo	Q0Make.vo 	\
+ QifMake.vo 	QbiMake.vo 	BigQ.vo )
+
+RATIONALVO:=$(RATIONALBIGVO)
+
+NUMBERSVO:= $(NUMBERSCOMMONVO) $(NATURALVO) $(INTEGERVO) $(NATINTVO) $(CYCLICVO) $(RATIONALVO)
+
+SETOIDSVO:=$(addprefix theories/Setoids/, \
+ Setoid.vo ) 
+
+UNICODEVO:=$(addprefix theories/Unicode/, \
+ Utf8.vo )
+
+CLASSESVO:=$(addprefix theories/Classes/, \
+ Init.vo	RelationClasses.vo	Morphisms.vo	Morphisms_Prop.vo \
+ Morphisms_Relations.vo	Functions.vo 	Equivalence.vo  SetoidTactics.vo  \
+ SetoidClass.vo 	SetoidAxioms.vo EquivDec.vo 	SetoidDec.vo )
 
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
   $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) \
   $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
-  $(INTSVO) $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO)
+  $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO)
 
 THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
 
 ## Contribs
 
-OMEGAVO:=\
- contrib/omega/PreOmega.vo contrib/omega/OmegaLemmas.vo contrib/omega/Omega.vo
-
-ROMEGAVO:=\
- contrib/romega/ReflOmegaCore.vo contrib/romega/ROmega.vo 
-
-RINGVO:=\
- contrib/ring/LegacyArithRing.vo      	contrib/ring/Ring_normalize.vo \
- contrib/ring/LegacyRing_theory.vo	contrib/ring/LegacyRing.vo \
- contrib/ring/LegacyNArithRing.vo     \
- contrib/ring/LegacyZArithRing.vo	contrib/ring/Ring_abstract.vo \
- contrib/ring/Quote.vo			contrib/ring/Setoid_ring_normalize.vo \
- contrib/ring/Setoid_ring.vo		contrib/ring/Setoid_ring_theory.vo
-
-FIELDVO:=\
- contrib/field/LegacyField_Compl.vo     contrib/field/LegacyField_Theory.vo \
- contrib/field/LegacyField_Tactic.vo    contrib/field/LegacyField.vo
-
-NEWRINGVO:=\
- contrib/setoid_ring/BinList.vo   	contrib/setoid_ring/Ring_theory.vo \
- contrib/setoid_ring/Ring_polynom.vo	contrib/setoid_ring/Ring_tac.vo \
- contrib/setoid_ring/Ring_base.vo 	contrib/setoid_ring/InitialRing.vo \
- contrib/setoid_ring/Ring_equiv.vo 	contrib/setoid_ring/Ring.vo \
- contrib/setoid_ring/ArithRing.vo	contrib/setoid_ring/NArithRing.vo \
- contrib/setoid_ring/ZArithRing.vo \
- contrib/setoid_ring/Field_theory.vo	contrib/setoid_ring/Field_tac.vo \
- contrib/setoid_ring/Field.vo		contrib/setoid_ring/RealField.vo
+OMEGAVO:=$(addprefix contrib/omega/, \
+ PreOmega.vo	OmegaLemmas.vo 	Omega.vo )
+
+ROMEGAVO:=$(addprefix contrib/romega/, \
+ ReflOmegaCore.vo 	ROmega.vo )
+
+RINGVO:=$(addprefix contrib/ring/, \
+ LegacyArithRing.vo	Ring_normalize.vo \
+ LegacyRing_theory.vo	LegacyRing.vo \
+ LegacyNArithRing.vo    \
+ LegacyZArithRing.vo	Ring_abstract.vo \
+ Quote.vo		Setoid_ring_normalize.vo \
+ Setoid_ring.vo		Setoid_ring_theory.vo )
+
+FIELDVO:=$(addprefix contrib/field/, \
+ LegacyField_Compl.vo   LegacyField_Theory.vo \
+ LegacyField_Tactic.vo  LegacyField.vo )
+
+NEWRINGVO:=$(addprefix contrib/setoid_ring/, \
+ BinList.vo   		Ring_theory.vo \
+ Ring_polynom.vo	Ring_tac.vo \
+ Ring_base.vo 		InitialRing.vo \
+ Ring_equiv.vo 		Ring.vo \
+ ArithRing.vo		NArithRing.vo \
+ ZArithRing.vo		\
+ Field_theory.vo	Field_tac.vo \
+ Field.vo		RealField.vo )
 
 XMLVO:= 
 
-FOURIERVO:=\
- contrib/fourier/Fourier_util.vo    contrib/fourier/Fourier.vo
+FOURIERVO:=$(addprefix contrib/fourier/, \
+ Fourier_util.vo    	Fourier.vo )
 
 FUNINDVO:= 
 
-RECDEFVO:=contrib/funind/Recdef.vo
+RECDEFVO:=$(addprefix contrib/funind/, \
+ Recdef.vo )
 
 JPROVERVO:= 
 
 CCVO:=
 
-DPVO:=contrib/dp/Dp.vo 
+DPVO:=$(addprefix contrib/dp/, \
+ Dp.vo )
 
-SUBTACVO:=theories/Program/Tactics.vo theories/Program/Equality.vo theories/Program/Subset.vo \
-	theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Basics.vo \
-	theories/Program/FunctionalExtensionality.vo theories/Program/Combinators.vo \
-	theories/Program/Syntax.vo theories/Program/Program.vo 
+SUBTACVO:=$(addprefix theories/Program/, \
+ Tactics.vo 	Equality.vo 	Subset.vo	Utils.vo 	\
+ Wf.vo 		Basics.vo	FunctionalExtensionality.vo 	\
+ Combinators.vo	Syntax.vo 	Program.vo )
 
-RTAUTOVO:= \
- contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo
+RTAUTOVO:=$(addprefix contrib/rtauto/, \
+ Bintree.vo	Rtauto.vo )
 
 CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
 	    $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) \
diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml
index 4528fde9c..7a1b55a11 100644
--- a/parsing/g_intsyntax.ml
+++ b/parsing/g_intsyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 (* digit-based syntax for int31, bigN bigZ and bigQ *)
 
@@ -28,7 +28,7 @@ let make_kn dir id = Libnames.encode_kn (make_dir dir) (Names.id_of_string id)
 
 
 (* int31 stuff *)
-let int31_module = ["Coq"; "Ints"; "Int31"]
+let int31_module = ["Coq"; "Numbers"; "Cyclic"; "Int31"; "Int31"]
 let int31_path = make_path int31_module "int31"
 let int31_id = make_kn int31_module
 let int31_scope = "int31_scope"
@@ -40,14 +40,14 @@ let int31_1 = ConstructRef ((int31_id "digits",0),2)
 
 
 (* bigN stuff*)
-let zn2z_module = ["Coq"; "Ints"; "Basic_type"]
+let zn2z_module = ["Coq"; "Numbers"; "Cyclic"; "DoubleCyclic"; "Basic_type"]
 let zn2z_path = make_path zn2z_module "zn2z"
 let zn2z_id = make_kn zn2z_module
 
 let zn2z_W0 = ConstructRef ((zn2z_id "zn2z",0),1)
 let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2)
 
-let bigN_module = ["Coq"; "Ints"; "BigN"]
+let bigN_module = ["Coq"; "Numbers"; "Natural"; "BigN"; "BigN"]
 let bigN_path = make_path bigN_module "bigN"
 (* big ugly hack *)
 let bigN_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigN_module)), 
@@ -78,7 +78,7 @@ let bigN_constructor =
 	       )
 
 (*bigZ stuff*)
-let bigZ_module = ["Coq"; "Ints"; "BigZ"]
+let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ"]
 let bigZ_path = make_path bigZ_module "bigZ"
 (* big ugly hack bis *)
 let bigZ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)), 
@@ -91,8 +91,8 @@ let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2)
 
 
 (*bigQ stuff*)
-let bigQ_module = ["Coq"; "Ints"; "num"; "BigQ"]
-let qmake_module = ["Coq"; "Ints"; "num"; "QMake_base"]
+let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"]
+let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake_base"]
 let bigQ_path = make_path bigQ_module "bigQ"
 (* big ugly hack bis *)
 let bigQ_id = make_kn qmake_module
diff --git a/theories/Ints/num/MemoFn.v b/theories/Lists/StreamMemo.v
index 7d2c7af01..bdbe0eccc 100644
--- a/theories/Ints/num/MemoFn.v
+++ b/theories/Lists/StreamMemo.v
@@ -7,32 +7,27 @@
 (************************************************************************)
 
 Require Import Eqdep_dec.
+Require Import Streams.
+
+(** * Memoization *)
+
+(** Successive outputs of a given function [f] are stored in 
+    a stream in order to avoid duplicated computations. *) 
 
 Section MemoFunction.
 
 Variable A: Type.
 Variable f: nat -> A.
-Variable g: A -> A.
-
-Hypothesis Hg_correct: forall n, f (S n) = g (f n).
-  
-(* Memo Stream *)
-CoInductive MStream: Type :=
- MSeq : A -> MStream -> MStream.
 
-(* Hd and Tl function *)
-Definition mhd (x: MStream) := 
-  let (a,s) := x in a.
-Definition mtl (x: MStream) := 
-  let (a,s) := x in s.
-
-CoFixpoint memo_make (n: nat): MStream:= MSeq (f n) (memo_make (S n)).
+CoFixpoint memo_make (n:nat) : Stream A := Cons (f n) (memo_make (S n)).
 
 Definition memo_list := memo_make 0.
 
-Fixpoint memo_get (n: nat) (l: MStream) {struct n}: A :=
-  match n with O => mhd l | S n1 => 
-     memo_get n1 (mtl l) end.
+Fixpoint memo_get (n:nat) (l:Stream A) : A :=
+  match n with 
+    | O => hd l 
+    | S n1 => memo_get n1 (tl l)
+  end.
 
 Theorem memo_get_correct: forall n, memo_get n memo_list = f n.
 Proof.
@@ -44,13 +39,21 @@ intros n; apply trans_equal with (f (n + 0)); try exact (F1 n 0).
 rewrite <- plus_n_O; auto.
 Qed.
 
-(* Building with possible sharing using g *)
-CoFixpoint imemo_make (fn: A): MStream :=
+(** Building with possible sharing using a iterator [g] :
+    We now suppose in addition that [f n] is in fact the [n]-th
+    iterate of a function [g].
+*)
+
+Variable g: A -> A.
+
+Hypothesis Hg_correct: forall n, f (S n) = g (f n).
+
+CoFixpoint imemo_make (fn:A) : Stream A :=
   let fn1 := g fn in 
-  MSeq fn1 (imemo_make fn1).
+  Cons fn1 (imemo_make fn1).
 
 Definition imemo_list := let f0 := f 0 in
-  MSeq f0 (imemo_make f0).
+  Cons f0 (imemo_make f0).
 
 Theorem imemo_get_correct: forall n, memo_get n imemo_list = f n.
 Proof.
@@ -65,13 +68,14 @@ Qed.
 
 End MemoFunction.
 
+(** For a dependent function, the previous solution is 
+    reused thanks to a temporarly hiding of the dependency
+    in a "container" [memo_val]. *)
+
 Section DependentMemoFunction.
 
 Variable A: nat -> Type.
 Variable f: forall n, A n.
-Variable g: forall n, A n -> A (S n).
-
-Hypothesis Hg_correct: forall n, f (S n) = g n (f n).
 
 Inductive memo_val: Type :=
   memo_mval: forall n, A n -> memo_val.
@@ -101,16 +105,11 @@ match v with
 end.
 
 Let mf n :=  memo_mval n (f n).
-Let mg v :=  match v with 
-             memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end.
-
 
 Definition dmemo_list := memo_list _ mf.
 
 Definition dmemo_get n l := memo_get_val n (memo_get _ n l).
 
-Definition dimemo_list := imemo_list _ mf mg.
-
 Theorem dmemo_get_correct: forall n, dmemo_get n dmemo_list = f n.
 Proof.
 intros n; unfold dmemo_get, dmemo_list.
@@ -129,6 +128,17 @@ assert (e = refl_equal n).
 rewrite H; auto.
 Qed.
 
+(** Finally, a version with both dependency and iterator *)
+
+Variable g: forall n, A n -> A (S n).
+
+Hypothesis Hg_correct: forall n, f (S n) = g n (f n).
+
+Let mg v :=  match v with 
+             memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end.
+
+Definition dimemo_list := imemo_list _ mf mg.
+
 Theorem dimemo_get_correct: forall n, dmemo_get n dimemo_list = f n.
 Proof.
 intros n; unfold dmemo_get, dimemo_list.
@@ -150,17 +160,20 @@ Qed.
 
 End DependentMemoFunction.
 
-(* An example with the memo function on factorial *)
+(** An example with the memo function on factorial *)
 
 (*
 Require Import ZArith.
+Open Scope Z_scope.
 
-Fixpoint tfact (n: nat) {struct n} := 
-  match n with O => 1%Z | 
-               S n1 => (Z_of_nat n * tfact n1)%Z end.
+Fixpoint tfact (n: nat) := 
+  match n with 
+   | O => 1 
+   | S n1 => Z_of_nat n * tfact n1 
+  end.
 
 Definition lfact_list := 
-  dimemo_list _ tfact (fun n z => (Z_of_nat (S  n) * z)%Z). 
+  dimemo_list _ tfact (fun n z => (Z_of_nat (S  n) * z)).
 
 Definition lfact n := dmemo_get _ tfact n lfact_list.
 
@@ -170,16 +183,23 @@ intros n; unfold lfact, lfact_list.
 rewrite dimemo_get_correct; auto.
 Qed.
 
-Fixpoint nop p := match p with
-xH => 0 | xI p1 => nop p1 | xO p1 => nop p1 end.
+Fixpoint nop p := 
+  match p with
+   | xH => 0 
+   | xI p1 => nop p1 
+   | xO p1 => nop p1 
+  end.
 
-Fixpoint test z := match z with
-Z0 => 0 | Zpos p1 => nop p1 | Zneg p1 => nop p1 end.
+Fixpoint test z := 
+  match z with
+   | Z0 => 0 
+   | Zpos p1 => nop p1 
+   | Zneg p1 => nop p1 
+  end.
 
 Time Eval vm_compute in test (lfact 2000).
 Time Eval vm_compute in test (lfact 2000).
 Time Eval vm_compute in test (lfact 1500).
 Time Eval vm_compute in (lfact 1500).
-
 *)
  
diff --git a/theories/Ints/Zaux.v b/theories/Numbers/BigNumPrelude.v
index 8e4b1d64f..8e4b1d64f 100644
--- a/theories/Ints/Zaux.v
+++ b/theories/Numbers/BigNumPrelude.v
diff --git a/theories/Ints/num/ZnZ.v b/theories/Numbers/Cyclic/Abstract/ZnZ.v
index d5b798a18..dfe091209 100644
--- a/theories/Ints/num/ZnZ.v
+++ b/theories/Numbers/Cyclic/Abstract/ZnZ.v
@@ -8,7 +8,7 @@
 (*        Benjamin Gregoire, INRIA          Laurent Thery, INRIA        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 (** * Signature and specification of a bounded integer structure *)
 
diff --git a/theories/Ints/Basic_type.v b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
index 2116aaddd..2116aaddd 100644
--- a/theories/Ints/Basic_type.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
diff --git a/theories/Ints/num/GenAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v
index fae16aad6..889ccaa4d 100644
--- a/theories/Ints/num/GenAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v
@@ -16,7 +16,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenBase.v b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
index e93e3a489..2283e3ca0 100644
--- a/theories/Ints/num/GenBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 (** * *)
 
@@ -20,7 +20,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import JMeq.
 
diff --git a/theories/Ints/num/GenDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v
index ea6868a90..0e9993b10 100644
--- a/theories/Ints/num/GenDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import GenBase.
 Require Import GenDivn1.
diff --git a/theories/Ints/num/GenDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v
index 3c70adb61..a686f0c27 100644
--- a/theories/Ints/num/GenDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenLift.v b/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v
index f74cdc30b..5f8b00a52 100644
--- a/theories/Ints/num/GenLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenMul.v b/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v
index 9a56f1ee3..57cdeeb88 100644
--- a/theories/Ints/num/GenMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v
index 63a0930ed..f8cb16858 100644
--- a/theories/Ints/num/GenSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/GenSub.v b/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v
index 6ffb24575..b96d09562 100644
--- a/theories/Ints/num/GenSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import GenBase.
 
diff --git a/theories/Ints/num/Zn2Z.v b/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v
index 48cf26840..9b77cf039 100644
--- a/theories/Ints/num/Zn2Z.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v
@@ -9,7 +9,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import GenBase.
 Require Import GenAdd.
diff --git a/theories/Ints/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index d7e80d4a2..d7e80d4a2 100644
--- a/theories/Ints/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
diff --git a/theories/Ints/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 8c7c1f809..8c7c1f809 100644
--- a/theories/Ints/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
diff --git a/theories/Ints/num/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 75fc19584..da65d276f 100644
--- a/theories/Ints/num/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 
 Open Scope Z_scope.
 
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index f81c71d72..2bb9bec4b 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -8,13 +8,13 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 Require Export NZAxioms.
 Require Import NMake. (* contains W0Type *)
 Require Import ZnZ.
 Require Import Basic_type. (* contains base *)
-Require Import Zaux.
+Require Import BigNumPrelude.
 
 Module NZBigIntsAxiomsMod (Import BoundedIntsMod : W0Type) <: NZAxiomsSig.
 
diff --git a/theories/Ints/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index b64a853fd..b64a853fd 100644
--- a/theories/Ints/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
diff --git a/theories/Ints/num/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 8cb779350..6705c1898 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -17,7 +17,7 @@
 - Remark: File automatically generated
 *)
 
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import ZArith.
 Require Import Basic_type.
 Require Import ZnZ.
@@ -26,7 +26,7 @@ Require Import Nbasic.
 Require Import GenMul.
 Require Import GenDivn1.
 Require Import Wf_nat.
-Require Import MemoFn.
+Require Import StreamMemo.
 
 Module Type W0Type.
  Parameter w : Set.
diff --git a/theories/Ints/num/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 1398e8f55..3d20c35ce 100644
--- a/theories/Ints/num/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Basic_type.
 Require Import Max.
 Require Import GenBase.
diff --git a/theories/Ints/num/genN.ml b/theories/Numbers/Natural/BigN/genN.ml
index 8bf583ab6..8bf583ab6 100644
--- a/theories/Ints/num/genN.ml
+++ b/theories/Numbers/Natural/BigN/genN.ml
diff --git a/theories/Ints/num/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 33e5f669c..33e5f669c 100644
--- a/theories/Ints/num/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
diff --git a/theories/Ints/num/Q0Make.v b/theories/Numbers/Rational/BigQ/Q0Make.v
index d5809ea59..e075bdb15 100644
--- a/theories/Ints/num/Q0Make.v
+++ b/theories/Numbers/Rational/BigQ/Q0Make.v
@@ -9,7 +9,7 @@
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
diff --git a/theories/Ints/num/QMake_base.v b/theories/Numbers/Rational/BigQ/QMake_base.v
index 0cd2d2122..e12c78581 100644
--- a/theories/Ints/num/QMake_base.v
+++ b/theories/Numbers/Rational/BigQ/QMake_base.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
+(* $Id$ *)
 
 (** * An implementation of rational numbers based on big integers *)
 
diff --git a/theories/Ints/num/QbiMake.v b/theories/Numbers/Rational/BigQ/QbiMake.v
index a98fda9d7..8420a5360 100644
--- a/theories/Ints/num/QbiMake.v
+++ b/theories/Numbers/Rational/BigQ/QbiMake.v
@@ -9,7 +9,7 @@
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
diff --git a/theories/Ints/num/QifMake.v b/theories/Numbers/Rational/BigQ/QifMake.v
index 83c182ee0..6df06bdf2 100644
--- a/theories/Ints/num/QifMake.v
+++ b/theories/Numbers/Rational/BigQ/QifMake.v
@@ -9,7 +9,7 @@
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
diff --git a/theories/Ints/num/QpMake.v b/theories/Numbers/Rational/BigQ/QpMake.v
index a28434baf..a194431ec 100644
--- a/theories/Ints/num/QpMake.v
+++ b/theories/Numbers/Rational/BigQ/QpMake.v
@@ -9,7 +9,7 @@
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.
diff --git a/theories/Ints/num/QvMake.v b/theories/Numbers/Rational/BigQ/QvMake.v
index 85655dafc..1282c8694 100644
--- a/theories/Ints/num/QvMake.v
+++ b/theories/Numbers/Rational/BigQ/QvMake.v
@@ -9,7 +9,7 @@
 Require Import Bool.
 Require Import ZArith.
 Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
 Require Import Arith.
 Require Export BigN.
 Require Export BigZ.