diff options
Diffstat (limited to 'theories/Structures/OrderTac.v')
| -rw-r--r-- | theories/Structures/OrderTac.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v index 43df377c0..2465dc539 100644 --- a/theories/Structures/OrderTac.v +++ b/theories/Structures/OrderTac.v @@ -53,7 +53,7 @@ Local Infix "+" := trans_ord. Module Type TotalOrder_NoInline <: TotalOrder. Parameter Inline t : Type. Parameters eq lt le : t -> t -> Prop. - Include Type IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal. + Include IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal. End TotalOrder_NoInline. Module Type TotalOrder_NoInline' := TotalOrder_NoInline <+ EqLtLeNotation. @@ -302,7 +302,7 @@ Definition t := O.t. Definition eq := O.eq. Definition lt := flip O.lt. Definition le := flip O.le. -Include Type EqLtLeNotation. +Include EqLtLeNotation. Instance eq_equiv : Equivalence eq. |