diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-17 13:31:12 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-17 13:31:12 +0000 |
| commit | 0768a9c968dfc205334dabdd3e86d2a91bb7a33a (patch) | |
| tree | 162a3910024fe2e2d23e88360ef1fc91f1798986 /theories/Structures/OrderedType.v | |
| parent | 77b71db8470553aed0476827ec2e39aed0cbb6ed (diff) | |
Simplification of OrdersTac thanks to the functor application ! with no inline
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12679 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Structures/OrderedType.v')
| -rw-r--r-- | theories/Structures/OrderedType.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 7d56d9666..72fbe7968 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -114,12 +114,11 @@ Module OrderedTypeFacts (Import O: OrderedType). Definition eq_equiv := eq_equiv. Definition lt_strorder := lt_strorder. Definition lt_compat := lt_compat. - Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x. - Proof. intros; destruct (compare x y); auto. Qed. + Definition lt_total := lt_total. Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y. Proof. unfold le; intuition. Qed. End OrderElts. - Module OrderTac := MakeOrderTac OrderElts. + Module OrderTac := !MakeOrderTac OrderElts. Ltac order := OrderTac.order. Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed. |