1 files changed, 6 insertions, 38 deletions
diff --git a/theories/Structures/DecidableType2Ex.v b/theories/Structures/DecidableType2Ex.v
index 7b9c052ec..2ce2b5662 100644
--- a/theories/Structures/DecidableType2Ex.v
+++ b/theories/Structures/DecidableType2Ex.v
@@ -8,61 +8,29 @@
 
 (* $Id$ *)
 
-Require Import DecidableType2.
+Require Import DecidableType2 Morphisms RelationPairs.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 (** * Examples of Decidable Type structures. *)
 
-(** A particular case of [DecidableType] where
-    the equality is the usual one of Coq. *)
-
-Module Type UsualDecidableType.
- Parameter Inline t : Type.
- Definition eq := @eq t.
- Program Instance eq_equiv : Equivalence eq.
- Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
-End UsualDecidableType.
-
-(** a [UsualDecidableType] is in particular an [DecidableType]. *)
-
-Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
-
-(** an shortcut for easily building a UsualDecidableType *)
-
-Module Type MiniDecidableType.
- Parameter Inline t : Type.
- Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }.
-End MiniDecidableType.
-
-Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
- Definition t:=M.t.
- Definition eq := @eq t.
- Program Instance eq_equiv : Equivalence eq.
- Definition eq_dec := M.eq_dec.
-End Make_UDT.
 
 (** From two decidable types, we can build a new DecidableType
    over their cartesian product. *)
 
 Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
 
- Definition t := prod D1.t D2.t.
+ Definition t := (D1.t * D2.t)%type.
 
- Definition eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y).
+ Definition eq := (D1.eq * D2.eq)%signature.
 
  Instance eq_equiv : Equivalence eq.
- Proof.
- constructor.
- intros (x1,x2); red; simpl; auto.
- intros (x1,x2) (y1,y2); unfold eq; simpl; intuition.
- intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto.
- Qed.
 
  Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
  Proof.
  intros (x1,x2) (y1,y2); unfold eq; simpl.
- destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); intuition.
+ destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
+  compute; intuition.
  Defined.
 
 End PairDecidableType.
@@ -70,7 +38,7 @@ End PairDecidableType.
 (** Similarly for pairs of UsualDecidableType *)
 
 Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
- Definition t := prod D1.t D2.t.
+ Definition t := (D1.t * D2.t)%type.
  Definition eq := @eq t.
  Program Instance eq_equiv : Equivalence eq.
  Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.