diff options
Diffstat (limited to 'theories/Structures/DecidableTypeEx.v')
| -rw-r--r-- | theories/Structures/DecidableTypeEx.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v index ac1f014b..971fcd7f 100644 --- a/theories/Structures/DecidableTypeEx.v +++ b/theories/Structures/DecidableTypeEx.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: DecidableTypeEx.v 12641 2010-01-07 15:32:52Z letouzey $ *) - Require Import DecidableType OrderedType OrderedTypeEx. Set Implicit Arguments. Unset Strict Implicit. @@ -81,9 +79,9 @@ End PairDecidableType. Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. Definition t := prod D1.t D2.t. Definition eq := @eq t. - Definition eq_refl := @refl_equal t. - Definition eq_sym := @sym_eq t. - Definition eq_trans := @trans_eq t. + Definition eq_refl := @eq_refl t. + Definition eq_sym := @eq_sym t. + Definition eq_trans := @eq_trans t. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. intros (x1,x2) (y1,y2); |