Avoid declaring hints about refl/sym/trans of eq in DecidableType2

 This used to be convenient in FSets, but since we now try to integrate
 DecidableType and OrderedType as foundation for other part of the stdlib,
 this should be avoided, otherwise some eauto take a _long_ time.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 37 insertions, 39 deletions

diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 0957ef2430..585b981366 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -24,9 +24,6 @@ End BareEquality.
 
 Module Type IsEq (Import E:BareEquality).
   Declare Instance eq_equiv : Equivalence eq.
-  Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv).
-  Hint Resolve (@Equivalence_Transitive _ _ eq_equiv).
-  Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv).
 End IsEq.
 
 (** * Earlier specification of equality by three separate lemmas. *)
diff --git a/theories/Structures/DecidableType2Facts.v b/theories/Structures/DecidableType2Facts.v
index 988122b0b5..154a40d872 100644
--- a/theories/Structures/DecidableType2Facts.v
+++ b/theories/Structures/DecidableType2Facts.v
@@ -49,22 +49,24 @@ Module KeyDecidableType(D:DecidableType).
 
   Instance eqk_equiv : Equivalence eqk.
   Proof.
-   constructor; eauto.
+   constructor; unfold eqk; repeat red; intros;
+   [ reflexivity | symmetry; auto | etransitivity; eauto ].
   Qed.
 
   Instance eqke_equiv : Equivalence eqke.
   Proof.
-   constructor. auto.
-   red; unfold eqke; intuition.
-   red; unfold eqke; intuition; [ eauto | congruence ].
+   constructor; unfold eqke; repeat red; intuition; simpl;
+   etransitivity; eauto.
   Qed.
 
+(*
   Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv).
   Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv).
   Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv).
   Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv).
   Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv).
   Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv).
+*)
 
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 49daacabda..0650546a5e 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -47,14 +47,14 @@ Module GenericMinMax (Import O:OrderedTypeFull) <: HasMinMax O.
    (lt x y /\ eq (max x y) y)  \/  (le y x /\ eq (max x y) x).
  Proof.
   intros. rewrite le_lteq. unfold max, gmax.
-  destruct (compare_spec x y); auto.
+  destruct (compare_spec x y); auto with relations.
  Qed.
 
  Lemma min_spec : forall x y,
    (lt x y /\ eq (min x y) x)  \/  (le y x /\ eq (min x y) y).
  Proof.
   intros. rewrite le_lteq. unfold min, gmin.
-  destruct (compare_spec x y); auto.
+  destruct (compare_spec x y); auto with relations.
  Qed.
 
 End GenericMinMax.
@@ -133,7 +133,7 @@ Defined.
 
 Lemma max_dec : forall n m, {max n m == n} + {max n m == m}.
 Proof.
- intros n m. apply max_case; auto.
+ intros n m. apply max_case; auto with relations.
  intros x y H [E|E]; [left|right]; order.
 Defined.
 
@@ -161,21 +161,19 @@ Qed.
 Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p.
 Proof.
  intros.
- destruct (M.max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq; auto.
- destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto.
- destruct (max_spec m p); intuition; order.
- destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto.
+ destruct (M.max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq.
+ destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'.
+ destruct (max_spec m p); intuition; order. order.
+ destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order.
  destruct (max_spec m p); intuition; order.
 Qed.
 
 Lemma max_comm : forall n m, max n m == max m n.
 Proof.
  intros.
- destruct (M.max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq; auto.
- destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto.
- order.
- destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto.
- order.
+ destruct (M.max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq.
+ destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
+ destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
 Qed.
 
 (** *** Least-upper bound properties of [max] *)
@@ -434,7 +432,7 @@ Lemma max_min_modular : forall n m p,
  max n (min m (max n p)) == min (max n m) (max n p).
 Proof.
  intros. rewrite <- max_min_distr.
- destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto.
+ destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E. reflexivity.
  destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'.
  rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto.
  rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto.
@@ -444,10 +442,10 @@ Lemma min_max_modular : forall n m p,
  min n (max m (min n p)) == max (min n m) (min n p).
 Proof.
  intros. rewrite <- min_max_distr.
- destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto.
+ destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E.
  destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'.
  rewrite 2 min_l; try OF.order. rewrite max_le_iff; right; OF.order.
- rewrite 2 min_l; try OF.order. rewrite max_le_iff; auto.
+ rewrite 2 min_l; try OF.order. rewrite max_le_iff; auto. reflexivity.
 Qed.
 
 (** Disassociativity *)
diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v
index 43b27553fb..3371977334 100644
--- a/theories/Structures/OrderedType2Alt.v
+++ b/theories/Structures/OrderedType2Alt.v
@@ -231,10 +231,10 @@ Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt.
  Proof.
  intros c x y z.
  destruct c; unfold compare.
- rewrite 3 compare_Eq; eauto.
- rewrite 3 compare_Lt. apply StrictOrder_Transitive.
+ rewrite 3 compare_Eq. etransitivity; eauto.
+ rewrite 3 compare_Lt. etransitivity; eauto.
  do 3 (rewrite compare_sym, CompOpp_iff, compare_Lt).
- intros; apply StrictOrder_Transitive with y; auto.
+ etransitivity; eauto.
  Qed.
 
 End OT_to_Alt.
diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v
index c64fb7a97b..1e45a3fbfb 100644
--- a/theories/Structures/OrderedType2Ex.v
+++ b/theories/Structures/OrderedType2Ex.v
@@ -58,9 +58,9 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
  (* transitive *)
  intros (x1,x2) (y1,y2) (z1,z2). compute. intuition.
  left; etransitivity; eauto.
- left; rewrite <- H0; auto.
- left; rewrite H; auto.
- right; split; eauto. etransitivity; eauto.
+ left. setoid_replace z1 with y1; auto with relations.
+ left; setoid_replace x1 with y1; auto with relations.
+ right; split; etransitivity; eauto.
  Qed.
 
  Instance lt_compat : Proper (eq==>eq==>iff) lt.
@@ -81,7 +81,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
  Proof.
  intros (x1,x2) (y1,y2); unfold compare; simpl.
  destruct (O1.compare_spec x1 y1); try (constructor; compute; auto).
- destruct (O2.compare_spec x2 y2); constructor; compute; auto.
+ destruct (O2.compare_spec x2 y2); constructor; compute; auto with relations.
  Qed.
 
 End PairOrderedType.
diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v
index e35c7c651c..9d964d7129 100644
--- a/theories/Structures/OrderedType2Facts.v
+++ b/theories/Structures/OrderedType2Facts.v
@@ -50,33 +50,34 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull).
 
  Module Order := OTF_to_OrderTac O.
  Ltac order := Order.order.
+ Ltac iorder := intuition order.
 
  Instance le_compat : Proper (eq==>eq==>iff) le.
- Proof. repeat red; intuition; order. Qed.
+ Proof. repeat red; iorder. Qed.
 
  Instance le_preorder : PreOrder le.
  Proof. split; red; order. Qed.
 
  Instance le_order : PartialOrder eq le.
- Proof. compute; intuition; order. Qed.
+ Proof. compute; iorder. Qed.
 
  Instance le_antisym : Antisymmetric _ eq le.
  Proof. apply partial_order_antisym; auto with *. Qed.
 
  Lemma le_not_gt_iff : forall x y, le x y <-> ~lt y x.
- Proof. split; order. Qed.
+ Proof. iorder. Qed.
 
  Lemma lt_not_ge_iff : forall x y, lt x y <-> ~le y x.
- Proof. split; order. Qed.
+ Proof. iorder. Qed.
 
  Lemma le_or_gt : forall x y, le x y \/ lt y x.
  Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
 
  Lemma lt_or_ge : forall x y, lt x y \/ le y x.
- Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
+ Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed.
 
  Lemma eq_is_le_ge : forall x y, eq x y <-> le x y /\ le y x.
- Proof. intuition; order. Qed.
+ Proof. iorder. Qed.
 
 End OrderedTypeFullFacts.
 
@@ -260,7 +261,7 @@ Definition compare := flip O.compare.
 Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
 Proof.
 intros; unfold compare, eq, lt, flip.
-destruct (O.compare_spec y x); auto.
+destruct (O.compare_spec y x); auto with relations.
 Qed.
 
 End OrderedTypeRev.
diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrderedType2Lists.v
index 567cbd9f85..51e7512393 100644
--- a/theories/Structures/OrderedType2Lists.v
+++ b/theories/Structures/OrderedType2Lists.v
@@ -197,7 +197,7 @@ Module KeyOrderedType(Import O:OrderedType).
     destruct H1 as [e' H2].
     elim (@ltk_not_eqk (k,e) (k,e')).
     eapply Sort_Inf_In; eauto.
-    red; simpl; auto.
+    repeat red; reflexivity.
   Qed.
 
   Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
@@ -211,8 +211,8 @@ Module KeyOrderedType(Import O:OrderedType).
   Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
       ltk e e' \/ eqk e e'.
   Proof.
-    intros; invlist InA; auto.
-    left; apply Sort_In_cons_1 with l; auto.
+    intros; invlist InA; auto with relations.
+    left; apply Sort_In_cons_1 with l; auto with relations.
   Qed.
 
   Lemma Sort_In_cons_3 :