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, 8 insertions, 9 deletions

diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v
index f383491d9..cad77b4eb 100644
--- a/theories/QArith/QOrderedType.v
+++ b/theories/QArith/QOrderedType.v
@@ -13,23 +13,22 @@ Local Open Scope Q_scope.
 
 (** * DecidableType structure for rational numbers *)
 
-Module Q_as_DT <: DecidableType.
+Module Q_as_DT <: DecidableTypeFull.
  Definition t := Q.
  Definition eq := Qeq.
  Instance eq_equiv : Equivalence Qeq.
- Definition eq_dec := Qeq_dec.
-
- (** The next fields are not mandatory, but allow [Q_as_DT] to be
-     also a [DecidableTypeOrig] (resp. a [BooleanEqualityType]). *)
- Definition eq_refl := Qeq_refl.
- Definition eq_sym := Qeq_sym.
- Definition eq_trans := eq_trans.
-
  Definition eqb := Qeq_bool.
  Definition eqb_eq := Qeq_bool_iff.
 
+ Include Self Backport_ET_fun. (** eq_refl, eq_sym, eq_trans *)
+ Include Self Bool2Dec_fun. (** eq_dec *)
+
 End Q_as_DT.
 
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
+
+
 
 (** * OrderedType structure for rational numbers *)