Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms

 We can now have a diamond-like approch to extentions of signatures,
 instead of a linear-only chains as earlier...

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

2 files changed, 14 insertions, 18 deletions

diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v
index c47b4b4fe..08391d33f 100644
--- a/theories/NArith/NOrderedType.v
+++ b/theories/NArith/NOrderedType.v
@@ -13,19 +13,17 @@ Local Open Scope N_scope.
 
 (** * DecidableType structure for [N] binary natural numbers *)
 
-Module N_as_MiniDT <: MiniDecidableType.
+Module N_as_UBE <: UsualBoolEq.
  Definition t := N.
- Definition eq_dec := N_eq_dec.
-End N_as_MiniDT.
-
-Module N_as_DT <: UsualDecidableType.
- Include Make_UDT N_as_MiniDT.
+ Definition eq := @eq N.
  Definition eqb := Neqb.
  Definition eqb_eq := Neqb_eq.
-End N_as_DT.
+End N_as_UBE.
+
+Module N_as_DT <: UsualDecidableTypeFull := Make_UDTF N_as_UBE.
 
-(** Note that [N_as_DT] can also be seen as a [DecidableType]
-    and a [DecidableTypeOrig] and a [BooleanEqualityType] *)
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
 
 
 
diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v
index b5629eabe..85667e29a 100644
--- a/theories/NArith/POrderedType.v
+++ b/theories/NArith/POrderedType.v
@@ -13,20 +13,18 @@ Local Open Scope positive_scope.
 
 (** * DecidableType structure for [positive] numbers *)
 
-Module Positive_as_MiniDT <: MiniDecidableType.
+Module Positive_as_UBE <: UsualBoolEq.
  Definition t := positive.
- Definition eq_dec := positive_eq_dec.
-End Positive_as_MiniDT.
-
-Module Positive_as_DT <: UsualDecidableType.
- Include Make_UDT Positive_as_MiniDT.
+ Definition eq := @eq positive.
  Definition eqb := Peqb.
  Definition eqb_eq := Peqb_eq.
-End Positive_as_DT.
+End Positive_as_UBE.
 
+Module Positive_as_DT <: UsualDecidableTypeFull
+ := Make_UDTF Positive_as_UBE.
 
-(** Note that [Positive_as_DT] can also be seen as a [DecidableType]
-    and a [DecidableTypeOrig] and a [BooleanEqualityType]. *)
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)