aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/NArith')
-rw-r--r--theories/NArith/NOrderedType.v16
-rw-r--r--theories/NArith/POrderedType.v16
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]. *)