From b37ceca4e2c6e39050ade2acef314dfed24c8e49 Mon Sep 17 00:00:00 2001
From: emakarov
Date: Thu, 4 Oct 2007 17:24:56 +0000
Subject: 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
---
 Makefile.common | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'Makefile.common')

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)
 
-- 
cgit v1.2.3