diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-18 11:29:23 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-18 11:29:23 +0000 |
commit | e4a667a4503de1ebda52aee4aa5e08fb0711f1ce (patch) | |
tree | c4ff3db280f0dd3ac6c132b701fc6073a4f6323e /theories/Structures/OrdersTac.v | |
parent | adf6390ab7bf96b0ffd699e96bd6b27bd9d99d98 (diff) |
Tentative de suppression de l'import automatique des hints et coercions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Structures/OrdersTac.v')
-rw-r--r-- | theories/Structures/OrdersTac.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 66a672c92..80871d102 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -87,6 +87,7 @@ Ltac subst_eqns := Definition interp_ord o := match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end. Local Notation "#" := interp_ord. +Import Morphisms_Prop. (* For Hints *) Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. Proof. @@ -267,19 +268,21 @@ End OT_to_OrderTac. Module TotalOrderRev (O:TotalOrder) <: TotalOrder. +Import O. Definition t := O.t. Definition eq := O.eq. Definition lt := flip O.lt. Definition le := flip O.le. Include EqLtLeNotation. +Import RelationClasses. (* For hints *) (* No Instance syntax to avoid saturating the Equivalence tables *) Definition eq_equiv := O.eq_equiv. Instance lt_strorder: StrictOrder lt. -Proof. unfold lt; auto with *. Qed. +Proof. unfold lt. auto using O.lt_strorder with *. Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. -Proof. unfold lt; auto with *. Qed. +Proof. unfold lt; auto using O.lt_compat with *. Qed. Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y. Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed. |