From d7e7e6756b46998e864cc00355d1946b69a43c1a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 27 Apr 2008 16:27:38 +0000
Subject: Suite r10857

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10858 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.common                             | 2 +-
 theories/Numbers/Integer/TreeMod/ZTreeMod.v | 6 +++---
 theories/Numbers/NatInt/Makefile            | 4 ----
 3 files changed, 4 insertions(+), 8 deletions(-)
 delete mode 100644 theories/Numbers/NatInt/Makefile

diff --git a/Makefile.common b/Makefile.common
index cf0f234d70..e45d70b996 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -561,7 +561,7 @@ ZARITHVO:=\
  theories/ZArith/ZOdiv_def.vo   theories/ZArith/ZOdiv.vo
 
 INTSVO:=\
- theories/Ints/Z/ZAux.vo \
+ 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 \
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index e885d25bc7..f81c71d728 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -8,13 +8,13 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i i*)
+(*i $Id:$ i*)
 
 Require Export NZAxioms.
 Require Import NMake. (* contains W0Type *)
 Require Import ZnZ.
-Require Import Basic_type. (* contais base *)
-Require Import ZAux.
+Require Import Basic_type. (* contains base *)
+Require Import Zaux.
 
 Module NZBigIntsAxiomsMod (Import BoundedIntsMod : W0Type) <: NZAxiomsSig.
 
diff --git a/theories/Numbers/NatInt/Makefile b/theories/Numbers/NatInt/Makefile
deleted file mode 100644
index e23d8dee24..0000000000
--- a/theories/Numbers/NatInt/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
-
-.v.vo:
-	coqtop -boot -compile $*
-- 
cgit v1.2.3