diff options
| author |  emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-29 14:07:44 +0000 |
|---|---|---|
| committer | emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-29 14:07:44 +0000 |
| commit | d6345cc90431f30247d6ff9d454d7fcb3178410e (patch) | |
| tree | 1f8cd7cd4850b9f06efb3cfb2091d7d79c5db2cb /Makefile | |
| parent | 555fc1fae7889911107904ed7f7f684a28950be8 (diff) | |
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
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 35 |
1 files changed, 34 insertions, 1 deletions
@@ -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 |