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

17 files changed, 102 insertions, 88 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 56186e623c..c08f46294c 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -581,6 +581,10 @@ Hint Unfold lt_tree gt_tree.
 Hint Resolve @ok.
 Hint Constructors Ok.
 
+(* TODO: modify proofs in order to avoid these hints *)
+Hint Resolve MX.eq_refl MX.eq_trans.
+Hint Immediate MX.eq_sym.
+
 Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h)
  "as" ident(s) :=
  set (s:=Node l x r h) in *; clearbody s; clear l x r h.
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 49f436a011..fe6c3c79c2 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -89,7 +89,7 @@ Qed.
 
 Lemma add_mem_1: mem x (add x s)=true.
 Proof.
-auto with set.
+auto with set relations.
 Qed.
 
 Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
@@ -99,7 +99,7 @@ Qed.
 
 Lemma remove_mem_1: mem x (remove x s)=false.
 Proof.
-rewrite <- not_mem_iff; auto with set.
+rewrite <- not_mem_iff; auto with set relations.
 Qed.
 
 Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
@@ -275,7 +275,7 @@ Qed.
 
 Lemma singleton_mem_1: mem x (singleton x)=true.
 Proof.
-auto with set.
+auto with set relations.
 Qed.
 
 Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
@@ -653,7 +653,7 @@ Lemma filter_add_1 : forall s x, f x = true ->
 Proof.
 red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
 intuition.
-rewrite <- H; apply Comp; auto.
+rewrite <- H; apply Comp; auto with relations.
 Qed.
 
 Lemma filter_add_2 : forall s x, f x = false ->
@@ -672,7 +672,7 @@ unfold Add, MP.Add; intros.
 repeat rewrite filter_iff; auto.
 rewrite H0; clear H0.
 intuition.
-setoid_replace y with x; auto.
+setoid_replace y with x; auto with relations.
 Qed.
 
 Lemma add_filter_2 : forall s s' x,
@@ -908,9 +908,9 @@ elim  (equal_2 H x); auto with set; intros.
 apply fold_equal with (eqA:=eqA); auto with set.
 transitivity (f x (fold f s0 i)).
 apply fold_add with (eqA:=eqA); auto with set.
-transitivity (g x (fold f s0 i)); auto with set.
-transitivity (g x (fold g s0 i)); auto with set.
-apply gc; auto with set.
+transitivity (g x (fold f s0 i)); auto with set relations.
+transitivity (g x (fold g s0 i)); auto with set relations.
+apply gc; auto with set relations.
 symmetry; apply fold_add with (eqA:=eqA); auto.
 do 2 rewrite fold_empty; reflexivity.
 Qed.
diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v
index bd99198f4b..84f6a17055 100644
--- a/theories/MSets/MSetFacts.v
+++ b/theories/MSets/MSetFacts.v
@@ -59,23 +59,23 @@ Lemma is_empty_2 : is_empty s = true -> Empty s.
 Proof. intros; apply -> is_empty_spec; auto. Qed.
 
 Lemma add_1 : E.eq x y -> In y (add x s).
-Proof. intros; apply <- add_spec; auto. Qed.
+Proof. intros; apply <- add_spec. auto with relations. Qed.
 Lemma add_2 : In y s -> In y (add x s).
 Proof. intros; apply <- add_spec; auto. Qed.
 Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.
-Proof. rewrite add_spec. intros H [H'|H']; auto. elim H; auto. Qed.
+Proof. rewrite add_spec. intros H [H'|H']; auto. elim H; auto with relations. Qed.
 
 Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
 Proof. intros; rewrite remove_spec; intuition. Qed.
 Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
-Proof. intros; apply <- remove_spec; auto. Qed.
+Proof. intros; apply <- remove_spec; auto with relations. Qed.
 Lemma remove_3 : In y (remove x s) -> In y s.
 Proof. rewrite remove_spec; intuition. Qed.
 
 Lemma singleton_1 : In y (singleton x) -> E.eq x y.
-Proof. rewrite singleton_spec; auto. Qed.
+Proof. rewrite singleton_spec; auto with relations. Qed.
 Lemma singleton_2 : E.eq x y -> In y (singleton x).
-Proof. rewrite singleton_spec; auto. Qed.
+Proof. rewrite singleton_spec; auto with relations. Qed.
 
 Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
 Proof. rewrite union_spec; auto. Qed.
@@ -190,7 +190,7 @@ Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s.
 Proof. rewrite add_spec; intuition. Qed.
 
 Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s)  <-> In y s).
-Proof. rewrite add_spec; intuition. elim H; auto. Qed.
+Proof. rewrite add_spec; intuition. elim H; auto with relations. Qed.
 
 Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y.
 Proof. rewrite remove_spec; intuition. Qed.
@@ -340,7 +340,7 @@ rewrite H0; intros.
 destruct H1 as (_,H1).
 apply H1; auto.
 rewrite H2.
-rewrite InA_alt; eauto.
+rewrite InA_alt. exists x0; split; auto with relations.
 Qed.
 
 Lemma exists_b : Proper (E.eq==>Logic.eq) f ->
@@ -354,7 +354,7 @@ rewrite <- H1; intros.
 destruct H0 as (H0,_).
 destruct H0 as (a,(Ha1,Ha2)); auto.
 exists a; split; auto.
-rewrite H2; rewrite InA_alt; eauto.
+rewrite H2; rewrite InA_alt; exists a; auto with relations.
 symmetry.
 rewrite H0.
 destruct H1 as (_,H1).
@@ -393,13 +393,12 @@ Instance mem_m : Proper (E.eq==>Equal==>Logic.eq) mem.
 Proof.
 intros x x' Hx s s' Hs.
 generalize (mem_iff s x). rewrite Hs, Hx at 1; rewrite mem_iff.
-destruct (mem x s); destruct (mem x' s'); intuition.
+destruct (mem x s), (mem x' s'); intuition.
 Qed.
 
 Instance singleton_m : Proper (E.eq==>Equal) singleton.
 Proof.
-intros x y H a.
-rewrite !singleton_iff; split; intros; etransitivity; eauto.
+intros x y H a. rewrite !singleton_iff, H; intuition.
 Qed.
 
 Instance add_m : Proper (E.eq==>Equal==>Equal) add.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index fbaa01c908..b21c00fe2b 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -830,7 +830,7 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O).
   rewrite (Ad y) in IN; destruct IN as [EQ|IN]. order.
   specialize (Ab y IN). order.
   left; split.
-  rewrite (Ad x); auto.
+  rewrite (Ad x). now left.
   intros y Hy. elim (Em y Hy).
  Qed.
 
@@ -844,9 +844,9 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O).
   split; intros [U|U]; try order.
   specialize (Ab1 y U). order.
   specialize (Ab2 y U). order.
-  rewrite (Ad1 x1); auto.
+  rewrite (Ad1 x1); auto with *.
   exists x2; repeat split; auto.
-  rewrite (Ad2 x2); auto.
+  rewrite (Ad2 x2); now left.
   intros y. rewrite (Ad2 y). intros [U|U]. order.
   specialize (Ab2 y U). order.
   Qed.
@@ -947,7 +947,7 @@ Module MakeListOrdering (O:OrderedType).
  Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 ->
   CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c.
  Proof.
-  destruct c; simpl; inversion_clear 2; auto.
+  destruct c; simpl; inversion_clear 2; auto with relations.
  Qed.
  Hint Resolve cons_CompSpec.
 
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index c5e300cdd4..4292eb9386 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -218,6 +218,11 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Notation Inf := (lelistA X.lt).
   Notation In := (InA X.eq).
 
+  (* TODO: modify proofs in order to avoid these hints *)
+  Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
+  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
+  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+
   Definition IsOk := Sort.
 
   Class Ok (s:t) : Prop := { ok : Sort s }.
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index 59fbcf49d8..dc82a14502 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -293,7 +293,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
    red; intros.
    apply (H a).
    rewrite elements_iff.
-   rewrite InA_alt; exists a; auto.
+   rewrite InA_alt; exists a; auto with relations.
   destruct (elements s); auto.
   elim (H0 e); simpl; auto.
   red; intros.
@@ -368,7 +368,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   apply Pempty. intro x. rewrite Hsame, InA_nil; intuition.
   (* step *)
   intros s Hsame; simpl.
-  apply Pstep' with (of_list l); auto.
+  apply Pstep' with (of_list l); auto with relations.
    inversion_clear Hdup; rewrite of_list_1; auto.
    red. intros. rewrite Hsame, of_list_1, InA_cons; intuition.
   apply IHl.
@@ -430,7 +430,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by
     (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto with *).
   clearbody l; clear Rstep s.
-  induction l; simpl; auto.
+  induction l; simpl; auto with relations.
   Qed.
 
   (** From the induction principle on [fold], we can deduce some general
@@ -546,7 +546,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   apply fold_rel with (R:=fun u v => eqA u (f x v)); intros.
   reflexivity.
   transitivity (f x0 (f x b)); auto.
-  apply Comp; auto.
+  apply Comp; auto with relations.
   Qed.
 
   (** ** Fold is a morphism *)
@@ -555,7 +555,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
    eqA (fold f s i) (fold f s i').
   Proof.
   intros. apply fold_rel with (R:=eqA); auto.
-  intros; apply Comp; auto.
+  intros; apply Comp; auto with relations.
   Qed.
 
   Lemma fold_equal :
@@ -597,7 +597,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   Proof.
   intros.
   symmetry.
-  apply fold_2 with (eqA:=eqA); auto with set.
+  apply fold_2 with (eqA:=eqA); auto with set relations.
   Qed.
 
   Lemma remove_fold_2: forall i s x, ~In x s ->
@@ -631,18 +631,18 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   apply equal_sym; apply union_Equal with x; auto with set.
   transitivity (f x (fold f (union s s') (fold f (inter s s') i))).
   apply fold_commutes; auto.
-  apply Comp; auto.
+  apply Comp; auto with relations.
   symmetry; apply fold_2 with (eqA:=eqA); auto.
   (* ~(In x s') *)
   transitivity (f x (fold f (union s s') (fold f (inter s'' s') i))).
   apply fold_2 with (eqA:=eqA); auto with set.
   transitivity (f x (fold f (union s s') (fold f (inter s s') i))).
-  apply Comp;auto.
+  apply Comp;auto with relations.
   apply fold_init;auto.
   apply fold_equal;auto.
   apply equal_sym; apply inter_Add_2 with x; auto with set.
   transitivity (f x (fold f s (fold f s' i))).
-  apply Comp; auto.
+  apply Comp; auto with relations.
   symmetry; apply fold_2 with (eqA:=eqA); auto.
   Qed.
 
@@ -738,7 +738,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   intros; rewrite FM.cardinal_1 in H.
   generalize (elements_2 (s:=s)).
   destruct (elements s); try discriminate.
-  exists e; auto.
+  exists e; auto with relations.
   Qed.
 
   Lemma cardinal_inv_2b :
@@ -758,8 +758,10 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   apply cardinal_1; rewrite <- H; auto.
   destruct (cardinal_inv_2 Heqn) as (x,H2).
   revert Heqn.
-  rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set.
-  rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set.
+  rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x));
+   auto with set relations.
+  rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x));
+   eauto with set relations.
   Qed.
 
   Instance cardinal_m : Proper (Equal==>Logic.eq) cardinal.
@@ -1053,7 +1055,7 @@ Module OrdProperties (M:Sets).
   apply X0 with (remove e s) e; auto with set.
   apply IHn.
   assert (S n = S (cardinal (remove e s))).
-   rewrite Heqn; apply cardinal_2 with e; auto with set.
+   rewrite Heqn; apply cardinal_2 with e; auto with set relations.
   inversion H0; auto.
   red; intros.
   rewrite remove_iff in H0; destruct H0.
@@ -1074,7 +1076,7 @@ Module OrdProperties (M:Sets).
   apply X0 with (remove e s) e; auto with set.
   apply IHn.
   assert (S n = S (cardinal (remove e s))).
-   rewrite Heqn; apply cardinal_2 with e; auto with set.
+   rewrite Heqn; apply cardinal_2 with e; auto with set relations.
   inversion H0; auto.
   red; intros.
   rewrite remove_iff in H0; destruct H0.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index c49ab9d95b..feab44f58b 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -119,6 +119,11 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   Notation NoDup := (NoDupA X.eq).
   Notation In := (InA X.eq).
 
+  (* TODO: modify proofs in order to avoid these hints *)
+  Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
+  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
+  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+
   Definition IsOk := NoDup.
 
   Class Ok (s:t) : Prop := { ok : NoDup s }.
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 15b8a9cd02..b57f8e27fb 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -498,6 +498,7 @@ Theorem add_mod: forall a b n, n~=0 -> 0 <= a*b ->
  (a+b) mod n == (a mod n + b mod n) mod n.
 Proof.
 intros a b n Hn Hab. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial.
+reflexivity.
 destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)];
  destruct (le_0_mul _ _ (mod_sign b n Hn)) as [(Hb',Hm)|(Hb',Hm)];
  auto using mul_nonneg_nonneg, mul_nonpos_nonpos.
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 12cf01cae8..5b81cadd2d 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -457,7 +457,7 @@ Qed.
 Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a * b) mod n == ((a mod n) * (b mod n)) mod n.
 Proof.
- intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial.
+ intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. reflexivity.
  now destruct (mod_bound b n).
 Qed.
 
@@ -468,7 +468,7 @@ Proof.
  generalize (add_nonneg_nonneg _ _ Ha Hb).
  rewrite (div_mod a n) at 1 2; [|order].
  rewrite <- add_assoc, add_comm, mul_comm.
- intros. rewrite mod_add; trivial.
+ intros. rewrite mod_add; trivial. reflexivity.
  apply add_nonneg_nonneg; auto. destruct (mod_bound a n); auto.
 Qed.
 
@@ -481,7 +481,7 @@ Qed.
 Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a+b) mod n == (a mod n + b mod n) mod n.
 Proof.
- intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial.
+ intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. reflexivity.
  now destruct (mod_bound b n).
 Qed.
 
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 2d627dbc79..6dcc9e91fe 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -164,8 +164,8 @@ Hypothesis Initial : initial init.
 Lemma initial_unique : forall m, initial m -> m == init.
 Proof.
 intros m Im. destruct (itersucc_or_itersucc init m) as (p,[H|H]).
-destruct p; simpl in *; auto. destruct (Initial _ H).
-destruct p; simpl in *; auto with *. destruct (Im _ H).
+destruct p. now simpl in *. destruct (Initial _ H).
+destruct p. now simpl in *. destruct (Im _ H).
 Qed.
 
 (** ... then all other points are descendant of it. *)
@@ -287,7 +287,7 @@ Qed.
 
 Lemma ofnat_succ : forall n, [Datatypes.S n] == succ [n].
 Proof.
- unfold ofnat. intros. simpl; auto.
+ now unfold ofnat.
 Qed.
 
 Lemma ofnat_pred : forall n, n<>O -> [Peano.pred n] == P [n].
@@ -336,7 +336,7 @@ Qed.
 
 Lemma ofnat_eq : forall n m, [n]==[m] <-> n = m.
 Proof.
-split. apply ofnat_injective. intros; subst; auto.
+split. apply ofnat_injective. intros; now subst.
 Qed.
 
 (* In addition, we can prove that [ofnat] preserves order. *)
@@ -382,8 +382,8 @@ Qed.
 Lemma ofnat_add : forall n m, [n+m] == [n]+[m].
 Proof.
  intros. rewrite ofnat_add_l.
- induction n; simpl; auto.
- rewrite ofnat_succ. apply succ_wd; auto.
+ induction n; simpl. reflexivity.
+ rewrite ofnat_succ. now apply succ_wd.
 Qed.
 
 Lemma ofnat_mul : forall n m, [n*m] == [n]*[m].
@@ -392,21 +392,21 @@ Proof.
  symmetry. apply mul_0_l.
  rewrite plus_comm.
  rewrite ofnat_succ, ofnat_add, mul_succ_l.
- apply add_wd; auto.
+ now apply add_wd.
 Qed.
 
 Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n.
 Proof.
  induction m; simpl; intros.
  rewrite ofnat_zero. apply sub_0_r.
- rewrite ofnat_succ, sub_succ_r. apply pred_wd; auto.
+ rewrite ofnat_succ, sub_succ_r. now apply pred_wd.
 Qed.
 
 Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].
 Proof.
  intros n m H. rewrite ofnat_sub_r.
  revert n H. induction m. intros.
- rewrite <- minus_n_O. simpl; auto.
+ rewrite <- minus_n_O. now simpl.
  intros.
  destruct n.
  inversion H.
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 :