From d6345cc90431f30247d6ff9d454d7fcb3178410e Mon Sep 17 00:00:00 2001
From: emakarov
Date: Fri, 29 Jun 2007 14:07:44 +0000
Subject: Added the directory theories/Numbers where axiomatizations and
 implementations (unary, binary, etc.) of different number classes (natural,
 integer, rational, real, complex, etc.) will be stored.Currently there are
 axiomatized natural numbers with two implementations and axiomatized
 integers. Modified Makefile accordingly but dod not include the new files in
 THEORIESVO yet.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9916 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 35 ++++++++++++++++++++++++++++++++++-
 1 file changed, 34 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 92f453590a..480bd53285 100644
--- a/Makefile
+++ b/Makefile
@@ -875,7 +875,7 @@ 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 \
@@ -1046,6 +1046,34 @@ REALSVO=$(REALSBASEVO) $(REALS_$(REALS))
 
 ALLREALS=$(REALSBASEVO) $(REALS_all)
 
+NUMBERSDIR=theories/Numbers
+NATURALDIR=$(NUMBERSDIR)/Natural
+NATAXIOMSDIR=$(NATURALDIR)/Axioms
+NATURALAXIOMSVO=\
+  $(NATAXIOMSDIR)/NAxioms.vo	$(NATAXIOMSDIR)/NDepRec.vo\
+  $(NATAXIOMSDIR)/NDomain.vo	$(NATAXIOMSDIR)/NLt.vo\
+  $(NATAXIOMSDIR)/NMiscFunct.vo	$(NATAXIOMSDIR)/NIso.vo\
+  $(NATAXIOMSDIR)/NOtherInd.vo	$(NATAXIOMSDIR)/NPlusLt.vo\
+  $(NATAXIOMSDIR)/NPlus.vo	$(NATAXIOMSDIR)/NStrongRec.vo\
+  $(NATAXIOMSDIR)/NTimesLt.vo	$(NATAXIOMSDIR)/NTimes.vo
+
+NATURALPEANOVO=$(NATURALDIR)/Peano/NPeano.vo
+NATURALBINARYVO=$(NATURALDIR)/Binary/NBinary.vo
+NATURALVO=$(NATURALAXIOMSVO) $(NATURALPEANOVO) $(NATURALBINARYVO)
+
+INTEGERDIR=$(NUMBERSDIR)/Integer
+INTAXIOMSDIR=$(INTEGERDIR)/Axioms
+INTEGERAXIOMSVO=\
+  $(INTAXIOMSDIR)/ZAxioms.vo	$(INTAXIOMSDIR)/ZDomain.vo\
+  $(INTAXIOMSDIR)/ZOrder.vo	$(INTAXIOMSDIR)/ZPlusOrder.vo\
+  $(INTAXIOMSDIR)/ZPlus.vo	$(INTAXIOMSDIR)/ZTimesOrder.vo\
+  $(INTAXIOMSDIR)/ZTimes.vo
+
+INTEGERNATPAIRSVO=$(INTEGERDIR)/NatPairs/ZNatPairs.vo
+INTEGERVO=$(INTEGERAXIOMSVO) $(INTEGERNATPAIRSVO)
+
+NUMBERSVO=$(NATURALVO) $(INTEGERVO)
+
 SETOIDSVO=theories/Setoids/Setoid.vo
 
 THEORIESVO =\
@@ -1079,6 +1107,11 @@ reals: $(REALSVO)
 allreals: $(ALLREALS)
 setoids: $(SETOIDSVO)
 sorting: $(SORTINGVO)
+# numbers
+natural: $(NATURALVO)
+integer: $(INTEGERVO)
+rational: $(RATIONALVO)
+numbers: $(NUMBERSVO)
 
 noreal: logic arith bool zarith qarith lists sets fsets intmap relations \
 	wellfounded setoids sorting
-- 
cgit v1.2.3