aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures')
-rw-r--r--theories/Structures/OrderedType.v7
1 files changed, 1 insertions, 6 deletions
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 6b9007fdd..c21d4fa0f 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -315,17 +315,12 @@ Module KeyOrderedType(O:OrderedType).
Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
Hint Immediate eqk_sym eqke_sym.
- Global Instance eqk_equiv : Equivalence eqk.
- Proof. split; eauto. Qed.
+ Global Instance eqk_equiv : Equivalence eqk.
Global Instance eqke_equiv : Equivalence eqke.
Proof. split; eauto. Qed.
Global Instance ltk_strorder : StrictOrder ltk.
- Proof.
- split; eauto.
- intros (x,e); compute; apply (StrictOrder_Irreflexive x).
- Qed.
Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
Proof.