diff options
| author | emakarov | 2007-10-04 17:24:56 +0000 |
|---|---|---|
| committer | emakarov | 2007-10-04 17:24:56 +0000 |
| commit | b37ceca4e2c6e39050ade2acef314dfed24c8e49 (patch) | |
| tree | 08c428a6fab03441ddfb60df21f5b6f535ef08a1 /Makefile.common | |
| parent | 302482baff728df7ed2ec2da5321278b9d3a7449 (diff) | |
Added the proof (in Numbers/Integers/TreeMod) that tree-like representation of integers due to Gregoire and Théry satisfies the axioms of integers without order. This refers to integers modulo n, i.e., those that fit trees of certain size, not to BigZ.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10178 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index ba790f62b6..08feab44b5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -531,7 +531,6 @@ INTSVO:=\ theories/Ints/Z/IntsZmisc.vo theories/Ints/Z/Pmod.vo \ theories/Ints/Tactic.vo theories/Ints/Z/ZAux.vo \ theories/Ints/Z/ZPowerAux.vo theories/Ints/Z/ZDivModAux.vo \ - theories/Ints/Z/Zmod.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 \ @@ -710,7 +709,9 @@ INTEGERBINARYVO:=$(INTEGERDIR)/Binary/ZBinary.vo INTEGERNATPAIRSVO:=$(INTEGERDIR)/NatPairs/ZNatPairs.vo -INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) +INTEGERTREEMODVO:=$(INTEGERDIR)/TreeMod/ZTreeMod.vo + +INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) $(INTEGERTREEMODVO) NUMBERSVO:=$(NATURALVO) $(INTEGERVO) |