New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))

 "Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for
 "Module M (...). Include M1. Include M2. Include M3... End M."

 Moreover M2,M3,etc can be functors as long as they find what they need in what
 comes before them (see new command "Include Self").
 The only real constraint is that M1,M2,M3,... should not have common elements
 (for the moment (?)).

 Same behavior for signature : Module Type M := M1 <+ M2 <+ M3.

 Note that this <+ is _not_ a primitive construct of the module language,
 for instance it cannot be used in signature (Module M <: M1 <+ M2 is
 illegal for the moment).

 Some example of use in Decidable2 and NZAxioms

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 30 deletions

diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index c85e84b04..889d9c2e5 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -23,7 +23,7 @@ Local Open Scope NumScope.
     for instance [Z/nZ] (See file [NZDomain for a study of that).
 *)
 
-Module Type NZDomain_fun (Import E : EqualityType).
+Module Type NZDomain (Import E : EqualityType).
  (** [E] provides [t], [eq], [eq_equiv : Equivalence eq] *)
 
 Notation "x == y"  := (eq x y) (at level 70) : NumScope.
@@ -47,21 +47,18 @@ Axiom bi_induction :
   forall A : t -> Prop, Proper (eq==>iff) A ->
     A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n.
 
-End NZDomain_fun.
+End NZDomain.
 
-Module Type NZDomainSig.
- Include Type EqualityType.
- Include Self Type NZDomain_fun.
-End NZDomainSig.
+Module Type NZDomainSig := EqualityType <+ NZDomain.
+
+(** A version with decidable type *)
+
+Module Type NZDecDomainSig := DecidableType <+ NZDomain.
 
-Module Type NZDecDomainSig.
- Include Type DecidableType.
- Include Self Type NZDomain_fun.
-End NZDecDomainSig.
 
 (** Axiomatization of basic operations : [+] [-] [*] *)
 
-Module Type NZBasicFuns_fun (Import NZ : NZDomainSig).
+Module Type NZHasBasicFuns (Import NZ : NZDomainSig).
 
 Parameter Inline add : t -> t -> t.
 Parameter Inline sub : t -> t -> t.
@@ -84,12 +81,10 @@ Axiom sub_succ_r : forall n m, n - (S m) == P (n - m).
 Axiom mul_0_l : forall n, 0 * n == 0.
 Axiom mul_succ_l : forall n m, S n * m == n * m + m.
 
-End NZBasicFuns_fun.
+End NZHasBasicFuns.
+
+Module Type NZBasicFunsSig := NZDomainSig <+ NZHasBasicFuns.
 
-Module Type NZBasicFunsSig.
- Include Type NZDomainSig.
- Include Self Type NZBasicFuns_fun.
-End NZBasicFunsSig.
 
 (** Old name for the same interface: *)
 
@@ -98,7 +93,7 @@ Module Type NZAxiomsSig := NZBasicFunsSig.
 
 (** Axiomatization of order *)
 
-Module Type NZOrd_fun (Import NZ : NZDomainSig).
+Module Type NZHasOrd (Import NZ : NZDomainSig).
 
 Parameter Inline lt : t -> t -> Prop.
 Parameter Inline le : t -> t -> Prop.
@@ -116,17 +111,14 @@ Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
 Axiom lt_irrefl : forall n, ~ (n < n).
 Axiom lt_succ_r : forall n m, n < S m <-> n <= m.
 
-End NZOrd_fun.
+End NZHasOrd.
 
-Module Type NZOrdSig.
- Include Type NZDomainSig.
- Include Self Type NZOrd_fun.
-End NZOrdSig.
+Module Type NZOrdSig := NZDomainSig <+ NZHasOrd.
 
 
 (** Axiomatization of minimum and maximum *)
 
-Module Type NZMinMax_fun (Import NZ : NZOrdSig).
+Module Type NZHasMinMax (Import NZ : NZOrdSig).
 
 Parameter Inline min : t -> t -> t.
 Parameter Inline max : t -> t -> t.
@@ -138,11 +130,9 @@ Axiom min_r : forall n m, m <= n -> min n m == m.
 Axiom max_l : forall n m, m <= n -> max n m == n.
 Axiom max_r : forall n m, n <= m -> max n m == m.
 
-End NZMinMax_fun.
+End NZHasMinMax.
+
+
+Module Type NZOrdAxiomsSig :=
+ NZDomainSig <+ NZHasBasicFuns <+ NZHasOrd <+ NZHasMinMax.
 
-Module Type NZOrdAxiomsSig.
- Include Type NZDomainSig.
- Include Self Type NZBasicFuns_fun.
- Include Self Type NZOrd_fun.
- Include Self Type NZMinMax_fun.
-End NZOrdAxiomsSig.