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

1 files changed, 7 insertions, 9 deletions

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]. *)