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, 10 deletions

diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
index 01e84a525..287d0c955 100644
--- a/theories/Arith/NatOrderedType.v
+++ b/theories/Arith/NatOrderedType.v
@@ -12,20 +12,17 @@ Require Import Lt Peano_dec Compare_dec EqNat
 
 (** * DecidableType structure for Peano numbers *)
 
-Module Nat_as_MiniDT <: MiniDecidableType.
+Module Nat_as_UBE <: UsualBoolEq.
  Definition t := nat.
- Definition eq_dec := eq_nat_dec.
-End Nat_as_MiniDT.
-
-Module Nat_as_DT <: UsualDecidableType.
- Include Make_UDT Nat_as_MiniDT.
- (** The next fields aren't mandatory but allow more subtyping. *)
+ Definition eq := @eq nat.
  Definition eqb := beq_nat.
  Definition eqb_eq := beq_nat_true_iff.
-End Nat_as_DT.
+End Nat_as_UBE.
+
+Module Nat_as_DT <: UsualDecidableTypeFull := Make_UDTF Nat_as_UBE.
 
-(** Note that [Nat_as_DT] can also be seen as a [DecidableType],
-    or a [DecidableTypeOrig] or a [BooleanEqualityType]. *)
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)