aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrderedType.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-01-07 15:32:22 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-01-07 15:32:22 +0000
commit345c0ee557465d7d2f22ac34898388dfbb57cd0f (patch)
treeba50e980e96fe1dd02183f8b89fd6b5ef5859ee6 /theories/Structures/OrderedType.v
parent56773377924f7f4d98d007b5687ebb44cff69042 (diff)
OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with Inline)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12636 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Structures/OrderedType.v')
-rw-r--r--theories/Structures/OrderedType.v12
1 files changed, 2 insertions, 10 deletions
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index f0d4163c3..ca441fc86 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -103,11 +103,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
Proof. intros; destruct (compare x y); auto. Qed.
- Module OrderElts : OrderSig
- with Definition t := t
- with Definition eq := eq
- with Definition lt := lt.
- (* Opaque signature is crucial for ltac to work correctly later *)
+ Module OrderElts <: OrderedType2.TotalOrder.
Definition t := t.
Definition eq := eq.
Definition lt := lt.
@@ -121,11 +117,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
Proof. unfold le; intuition. Qed.
End OrderElts.
Module OrderTac := MakeOrderTac OrderElts.
-
- Ltac order :=
- change eq with OrderElts.eq in *;
- change lt with OrderElts.lt in *;
- OrderTac.order.
+ Ltac order := OrderTac.order.
Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed.
Lemma eq_le x y z : eq x y -> ~lt y z -> ~lt x z. Proof. order. Qed.