From 70eb4b8dd94ef17cb246a25eb7525626e0f30296 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 5 Jan 2010 18:39:14 +0000
Subject: Numbers abstract layer: more Module Type, used especially for
 divisions.

 Properties are now rather passed as functor arg instead of via Include or
 some inner modules.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12629 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/Abstract/ZBase.v       | 2 +-
 theories/Numbers/Integer/Abstract/ZDivEucl.v    | 6 ++----
 theories/Numbers/Integer/Abstract/ZDivFloor.v   | 6 ++----
 theories/Numbers/Integer/Abstract/ZDivTrunc.v   | 6 ++----
 theories/Numbers/Integer/Abstract/ZMulOrder.v   | 2 +-
 theories/Numbers/Integer/Abstract/ZProperties.v | 7 ++++++-
 6 files changed, 14 insertions(+), 15 deletions(-)

(limited to 'theories/Numbers/Integer/Abstract')

diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 3429a4fa3d..64a122c714 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -15,7 +15,7 @@ Require Export ZAxioms.
 Require Import NZProperties.
 
 Module ZBasePropFunct (Import Z : ZAxiomsSig).
-Include NZPropFunct Z.
+Include Type NZPropFunct Z.
 Local Open Scope NumScope.
 
 (* Theorems that are true for integers but not for natural numbers *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index ad8e24cfb1..a853395a68 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -33,9 +33,7 @@ End ZDiv.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
 
-Module ZDivPropFunct (Import Z : ZDivSig).
- (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *)
- Module Import ZP := ZPropFunct Z.
+Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
@@ -48,7 +46,7 @@ Module ZDivPropFunct (Import Z : ZDivSig).
   apply le_trans with 0; [ rewrite opp_nonpos_nonneg |]; order.
   Qed.
  End Z'.
- Module Import NZDivP := NZDivPropFunct Z'.
+ Module Import NZDivP := NZDivPropFunct Z' ZP.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index fe695907d2..551ce6b410 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -36,9 +36,7 @@ End ZDiv.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
 
-Module ZDivPropFunct (Import Z : ZDivSig).
- (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *)
- Module Import ZP := ZPropFunct Z.
+Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
@@ -47,7 +45,7 @@ Module ZDivPropFunct (Import Z : ZDivSig).
   Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
   Proof. intros. now apply mod_pos_bound. Qed.
  End Z'.
- Module Import NZDivP := NZDivPropFunct Z'.
+ Module Import NZDivP := NZDivPropFunct Z' ZP.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index b57f8e27fb..c60bf7c6aa 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -37,13 +37,11 @@ End ZDiv.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
 
-Module ZDivPropFunct (Import Z : ZDivSig).
- (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *)
- Module Import ZP := ZPropFunct Z.
+Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
- Module Import NZDivP := NZDivPropFunct Z.
+ Module Import NZDivP := NZDivPropFunct Z ZP.
 
 Ltac pos_or_neg a :=
  let LT := fresh "LT" in
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index a9cf0dc4d3..bd9a857145 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -12,7 +12,7 @@
 
 Require Export ZAddOrder.
 
-Module ZMulOrderPropFunct (Import Z : ZAxiomsSig).
+Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig).
 Include ZAddOrderPropFunct Z.
 Local Open Scope NumScope.
 
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index eee5b0273a..7f22532059 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -15,4 +15,9 @@ Require Export ZAxioms ZMulOrder.
     subsumes all others.
 *)
 
-Module ZPropFunct := ZMulOrderPropFunct.
+Module Type ZPropSig := ZMulOrderPropFunct.
+
+Module ZPropFunct (Z:ZAxiomsSig) <: ZPropSig Z.
+ Include Type ZPropSig Z.
+End ZPropFunct.
+
-- 
cgit v1.2.3