From 5c97a67f3227f718a2247c9476029548c4ee8e28 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 29 Jan 2010 14:18:31 +0000
Subject: Division in numbers: kills some Include to avoid bad alias Zsucc =
 ZDiv.Z.Z'.S

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12704 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/NatInt/NZDiv.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'theories/Numbers/NatInt')

diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index b189d5b298..1f6c615bc3 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -43,11 +43,13 @@ End NZDivSpecific.
 Module Type NZDiv (NZ:NZOrdAxiomsSig)
  := DivMod NZ <+ NZDivCommon NZ <+ NZDivSpecific NZ.
 
-Module Type NZDivSig := NZOrdAxiomsSig <+ NZDiv.
-Module Type NZDivSig' := NZOrdAxiomsSig' <+ NZDiv <+ DivModNotation.
+Module Type NZDiv' (NZ:NZOrdAxiomsSig) := NZDiv NZ <+ DivModNotation NZ.
 
 Module NZDivPropFunct
- (Import NZ : NZDivSig')(Import NZP : NZMulOrderPropSig NZ).
+ (Import NZ : NZOrdAxiomsSig')
+ (Import NZP : NZMulOrderPropSig NZ)
+ (Import NZD : NZDiv' NZ)
+.
 
 (** Uniqueness theorems *)
 
-- 
cgit v1.2.3