[Stdlib] OrderedType: do not pollute the “core” hint database

6 files changed, 76 insertions, 75 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 8627ff7353..7c69350db4 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -593,14 +593,14 @@ Qed.
 Lemma MapsTo_1 :
  forall m x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m.
 Proof.
- induction m; simpl; intuition_in; eauto.
+ induction m; simpl; intuition_in; eauto with ordered_type.
 Qed.
 Hint Immediate MapsTo_1 : core.
 
 Lemma In_1 :
  forall m x y, X.eq x y -> In x m -> In y m.
 Proof.
- intros m x y; induction m; simpl; intuition_in; eauto.
+ intros m x y; induction m; simpl; intuition_in; eauto with ordered_type.
 Qed.
 
 Lemma In_node_iff :
@@ -671,7 +671,7 @@ Qed.
 Lemma lt_tree_trans :
  forall x y, X.lt x y -> forall m, lt_tree x m -> lt_tree y m.
 Proof.
- eauto.
+ eauto with ordered_type.
 Qed.
 
 Lemma gt_tree_not_in :
@@ -683,7 +683,7 @@ Qed.
 Lemma gt_tree_trans :
  forall x y, X.lt y x -> forall m, gt_tree x m -> gt_tree y m.
 Proof.
- eauto.
+ eauto with ordered_type.
 Qed.
 
 Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.
@@ -707,7 +707,7 @@ Qed.
 Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
 Proof.
  destruct m as [|r x e l h]; simpl; auto.
- intro H; elim (H x e); auto.
+ intro H; elim (H x e); auto with ordered_type.
 Qed.
 
 Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
@@ -732,7 +732,7 @@ Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e.
 Proof.
  intros m x; functional induction (find x m); auto; intros; clearf;
   inv bst; intuition_in; simpl; auto;
- try solve [order | absurd (X.lt x y); eauto | absurd (X.lt y x); eauto].
+ try solve [order | absurd (X.lt x y); eauto with ordered_type | absurd (X.lt y x); eauto with ordered_type].
 Qed.
 
 Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
@@ -832,8 +832,8 @@ Lemma bal_bst : forall l x e r, bst l -> bst r ->
 Proof.
  intros l x e r; functional induction (bal l x e r); intros; clearf;
  inv bst; repeat apply create_bst; auto; unfold create; try constructor;
- (apply lt_tree_node || apply gt_tree_node); auto;
- (eapply lt_tree_trans || eapply gt_tree_trans); eauto. 
+ (apply lt_tree_node || apply gt_tree_node); auto with ordered_type;
+ (eapply lt_tree_trans || eapply gt_tree_trans); eauto with ordered_type.
 Qed.
 Hint Resolve bal_bst : core.
 
@@ -865,7 +865,7 @@ Lemma add_in : forall m x y e,
 Proof.
  intros m x y e; functional induction (add x e m); auto; intros;
  try (rewrite bal_in, IHt); intuition_in.
- apply In_1 with x; auto.
+ apply In_1 with x; auto with ordered_type.
 Qed.
 
 Lemma add_bst : forall m x e, bst m -> bst (add x e m).
@@ -874,14 +874,14 @@ Proof.
   inv bst; try apply bal_bst; auto;
   intro z; rewrite add_in; intuition.
  apply MX.eq_lt with x; auto.
- apply MX.lt_eq with x; auto.
+ apply MX.lt_eq with x; auto with ordered_type.
 Qed.
 Hint Resolve add_bst : core.
 
 Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
 Proof.
  intros m x y e; functional induction (add x e m);
-   intros; inv bst; try rewrite bal_mapsto; unfold create; eauto.
+   intros; inv bst; try rewrite bal_mapsto; unfold create; eauto with ordered_type.
 Qed.
 
 Lemma add_2 : forall m x y e e', ~X.eq x y ->
@@ -912,7 +912,7 @@ Proof.
   intros; rewrite find_mapsto_equiv; auto.
   split; eauto using add_2, add_3.
  destruct X.compare; try (apply H0; order).
- auto using find_1, add_1.
+ auto using find_1, add_1 with ordered_type.
 Qed.
 
 (** * Extraction of minimum binding *)
@@ -971,7 +971,7 @@ Proof.
  generalize (remove_min_in ll lx ld lr _x m#1).
  rewrite e0; simpl; intros.
  rewrite (bal_in l' x d r y) in H.
- assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto); clear H4.
+ assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto with ordered_type); clear H4.
  assert (X.lt m#1 x) by order.
  decompose [or] H; order.
 Qed.
@@ -1050,7 +1050,7 @@ Proof.
  (* EQ *)
  inv bst; clear e0.
  rewrite merge_in; intuition; [ order | order | intuition_in ].
- elim H4; eauto.
+ elim H4; eauto with ordered_type.
  (* GT *)
  inv bst; clear e0.
  rewrite bal_in; auto.
@@ -1069,7 +1069,7 @@ Proof.
  destruct H; eauto.
  (* EQ *)
  inv bst.
- apply merge_bst; eauto.
+ apply merge_bst; eauto with ordered_type.
  (* GT *)
  inv bst.
  apply bal_bst; auto.
@@ -1124,8 +1124,8 @@ Lemma join_bst : forall l x d r, bst l -> bst r ->
 Proof.
  join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto;
  clear Hrl Hlr; intro; intros; rewrite join_in in *.
- intuition; [ apply MX.lt_eq with x | ]; eauto.
- intuition; [ apply MX.eq_lt with x | ]; eauto.
+ intuition; [ apply MX.lt_eq with x | ]; eauto with ordered_type.
+ intuition; [ apply MX.eq_lt with x | ]; eauto with ordered_type.
 Qed.
 Hint Resolve join_bst : core.
 
@@ -1135,8 +1135,8 @@ Lemma join_find : forall l x d r y,
 Proof.
  join_tac; auto; inv bst;
   simpl (join (Leaf elt));
-  try (assert (X.lt lx x) by auto);
-  try (assert (X.lt x rx) by auto);
+  try (assert (X.lt lx x) by auto with ordered_type);
+  try (assert (X.lt x rx) by auto with ordered_type);
   rewrite ?add_find, ?bal_find; auto.
 
  simpl; destruct X.compare; auto.
@@ -1260,7 +1260,7 @@ Proof.
  change (bst (m2',xd)#1). rewrite <-e1; eauto.
  intros y Hy.
  apply H1; auto.
- rewrite remove_min_in, e1; simpl; auto.
+ rewrite remove_min_in, e1; simpl; auto with ordered_type.
  change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto.
 Qed.
 Hint Resolve concat_bst : core.
@@ -1283,9 +1283,9 @@ Proof.
  simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto.
  destruct (find y m2'); auto.
  symmetry; rewrite not_find_iff; auto; intro.
- apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto.
+ apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto with ordered_type.
 
- intros z Hz; apply H1; auto; rewrite H3; auto.
+ intros z Hz; apply H1; auto; rewrite H3; auto with ordered_type.
 Qed.
 
 
@@ -1338,12 +1338,12 @@ Proof.
  apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6.
  destruct (elements_aux_mapsto r acc y' e'); intuition.
  red; simpl; eauto.
- red; simpl; eauto.
- intros.
+ red; simpl; eauto with ordered_type.
+ intros x e0 y0 H H6.
  inversion_clear H.
  destruct H7; simpl in *.
  order.
- destruct (elements_aux_mapsto r acc x e0); intuition eauto. 
+ destruct (elements_aux_mapsto r acc x e0); intuition eauto with ordered_type.
 Qed.
 
 Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s).
@@ -1567,7 +1567,7 @@ Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt),
     MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m).
 Proof.
 induction m; simpl; inversion_clear 1; auto.
-exists k; auto.
+exists k; auto with ordered_type.
 destruct (IHm1 _ _ H0).
 exists x0; intuition.
 destruct (IHm2 _ _ H0).
@@ -2072,7 +2072,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
    X.eq x1 x2 -> D.eq d1 d2 ->
    Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2).
   Proof.
-   destruct c; simpl; intros; P.MX.elim_comp; auto.
+   destruct c; simpl; intros; P.MX.elim_comp; auto with ordered_type.
   Qed.
   Hint Resolve cons_Cmp : core.
 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 1a531542cc..758f9d41b0 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -1822,7 +1822,7 @@ Module OrdProperties (M:S).
     destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); auto.
    unfold O.ltk in *; simpl in *; intros.
    symmetry; rewrite H2.
-   apply ME.eq_lt with a; auto.
+   apply ME.eq_lt with a; auto with ordered_type.
    rewrite <- H1; auto.
    unfold O.ltk in *; simpl in *; intros.
    rewrite H1.
@@ -1869,7 +1869,7 @@ Module OrdProperties (M:S).
   rewrite <- elements_mapsto_iff in H1.
   assert (~E.eq x t0).
    contradict H.
-   exists e0; apply MapsTo_1 with t0; auto.
+   exists e0; apply MapsTo_1 with t0; auto with ordered_type.
   ME.order.
   apply (@filter_sort _ eqke); auto with *; clean_eauto.
   intros.
@@ -1888,9 +1888,9 @@ Module OrdProperties (M:S).
     find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
     add_mapsto_iff by (auto with *).
   unfold O.eqke, O.ltk; simpl.
-  destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto.
+  destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto with ordered_type.
   - elim H; exists e0; apply MapsTo_1 with t0; auto.
-  - fold (~E.lt t0 x); auto.
+  - fold (~E.lt t0 x); auto with ordered_type.
   Qed.
 
   Lemma elements_Add_Above : forall m m' x e,
@@ -1905,7 +1905,7 @@ Module OrdProperties (M:S).
   destruct x0; destruct y.
   rewrite <- elements_mapsto_iff in H1.
   unfold O.eqke, O.ltk in *; simpl in *; destruct H3.
-  apply ME.lt_eq with x; auto.
+  apply ME.lt_eq with x; auto with ordered_type.
   apply H; firstorder.
   inversion H3.
   red; intros a; destruct a.
@@ -1991,7 +1991,7 @@ Module OrdProperties (M:S).
   injection H as [= -> ->].
   inversion_clear H1.
   red in H; simpl in *; intuition.
-  elim H0; eauto.
+  elim H0; eauto with ordered_type.
   inversion H.
   change (max_elt_aux (p::l) = Some (x,e)) in H.
   generalize (IHl x e H); clear IHl; intros IHl.
@@ -2007,9 +2007,9 @@ Module OrdProperties (M:S).
    inversion_clear H2.
    inversion_clear H5.
    red in H2; simpl in H2; ME.order.
-  eapply IHl; eauto.
+  eapply IHl; eauto with ordered_type.
   econstructor; eauto.
-  red; eauto.
+  red; eauto with ordered_type.
   inversion H2; auto.
   Qed.
 
@@ -2022,7 +2022,7 @@ Module OrdProperties (M:S).
   induction (elements m).
   simpl; try discriminate.
   destruct a; destruct l; simpl in *.
-  injection H; intros; subst; constructor; red; auto.
+  injection H; intros; subst; constructor; red; auto with ordered_type.
   constructor 2; auto.
   Qed.
 
@@ -2069,7 +2069,7 @@ Module OrdProperties (M:S).
   destruct (elements m).
   simpl; try discriminate.
   destruct p; simpl in *.
-  injection H; intros; subst; constructor; red; auto.
+  injection H; intros; subst; constructor; red; auto with ordered_type.
   Qed.
 
   Lemma min_elt_Empty :
@@ -2106,7 +2106,7 @@ Module OrdProperties (M:S).
   apply IHn.
   assert (S n = S (cardinal (remove k m))).
    rewrite Heqn.
-   eapply cardinal_2; eauto with map.
+   eapply cardinal_2; eauto with map ordered_type.
   inversion H1; auto.
   eapply max_elt_Above; eauto.
 
@@ -2133,7 +2133,7 @@ Module OrdProperties (M:S).
   apply IHn.
   assert (S n = S (cardinal (remove k m))).
    rewrite Heqn.
-   eapply cardinal_2; eauto with map.
+   eapply cardinal_2; eauto with map ordered_type.
   inversion H1; auto.
   eapply min_elt_Below; eauto.
 
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 8ca9401a06..0ef356b582 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -712,7 +712,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
    X.eq x1 x2 -> D.eq d1 d2 ->
    Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2).
   Proof.
-   destruct c; simpl; intros; MX.elim_comp; auto.
+   destruct c; simpl; intros; MX.elim_comp; auto with ordered_type.
   Qed.
   Hint Resolve cons_Cmp : core.
 
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index b21d809059..cad528644a 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -68,7 +68,7 @@ Proof.
  intros m.
  case m;auto.
  intros (k,e) l inlist.
- absurd (InA eqke (k, e) ((k, e) :: l));auto.
+ absurd (InA eqke (k, e) ((k, e) :: l)); auto with ordered_type.
 Qed.
 
 Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
@@ -106,14 +106,14 @@ Proof.
  elim (sort_inv sorted);auto.
  elim (In_inv belong1);auto.
  intro abs.
- absurd (X.eq x k');auto.
+ absurd (X.eq x k'); auto with ordered_type.
 Qed.
 
 Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m.
 Proof.
  intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo.
  functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail).
- exists _x; auto.
+ exists _x; auto with ordered_type.
  induction IHb; auto.
  exists x0; auto.
  inversion_clear sorted; auto.
@@ -135,7 +135,7 @@ Function find (k:key) (s: t elt) {struct s} : option elt :=
 Lemma find_2 :  forall m x e, find x m = Some e -> MapsTo x e m.
 Proof.
  intros m x. unfold PX.MapsTo.
- functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto.
+ functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto with ordered_type.
 Qed.
 
 Lemma find_1 :  forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e.
@@ -174,7 +174,7 @@ Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
 Proof.
  intros m x y e; generalize y; clear y.
  unfold PX.MapsTo.
- functional induction (add x e m);simpl;auto.
+ functional induction (add x e m);simpl;auto with ordered_type.
 Qed.
 
 Lemma add_2 : forall m x y e e',
@@ -195,12 +195,12 @@ Qed.
 
 Lemma add_3 : forall m x y e e',
   ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
-Proof.
+Proof with auto with ordered_type.
  intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl; intros.
- apply (In_inv_3 H0); compute; auto.
- apply (In_inv_3 H0); compute; auto.
- constructor 2; apply (In_inv_3 H0); compute; auto.
+ apply (In_inv_3 H0)...
+ apply (In_inv_3 H0)...
+ constructor 2; apply (In_inv_3 H0)...
  inversion_clear H0; auto.
 Qed.
 
@@ -254,7 +254,7 @@ Proof.
 
  clear e0;inversion_clear Hm.
  apply Sort_Inf_NotIn with x0; auto.
- apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto.
+ apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto with ordered_type.
 
  clear e0;inversion_clear Hm.
  assert (notin:~ In y (remove x l)) by auto.
@@ -374,13 +374,13 @@ Definition Equivb cmp m m' :=
 
 Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp,
   Equivb cmp m m' -> equal cmp m m' = true.
-Proof.
+Proof with auto with ordered_type.
  intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
  functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb;
  intuition; subst.
  match goal with H: X.compare _ _ = _ |- _ => clear H end.
  assert (cmp_e_e':cmp e e' = true).
-  apply H1 with x; auto.
+  apply H1 with x...
  rewrite cmp_e_e'; simpl.
  apply IHb; auto.
  inversion_clear Hm; auto.
@@ -388,7 +388,7 @@ Proof.
  unfold Equivb; intuition.
  destruct (H0 k).
  assert (In k ((x,e) ::l)).
-  destruct H as (e'', hyp); exists e''; auto.
+  destruct H as (e'', hyp); exists e''...
  destruct (In_inv (H2 H4)); auto.
  inversion_clear Hm.
  elim (Sort_Inf_NotIn H6 H7).
@@ -396,20 +396,20 @@ Proof.
  apply MapsTo_eq with k; auto; order.
  destruct (H0 k).
  assert (In k ((x',e') ::l')).
-  destruct H as (e'', hyp); exists e''; auto.
+  destruct H as (e'', hyp); exists e''...
  destruct (In_inv (H3 H4)); auto.
  inversion_clear Hm'.
  elim (Sort_Inf_NotIn H6 H7).
  destruct H as (e'', hyp); exists e''; auto.
  apply MapsTo_eq with k; auto; order.
- apply H1 with k; destruct (X.eq_dec x k); auto.
+ apply H1 with k; destruct (X.eq_dec x k)...
 
 
  destruct (X.compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y.
  destruct (H0 x).
  assert (In x ((x',e')::l')).
   apply H; auto.
-  exists e; auto.
+  exists e...
  destruct (In_inv H3).
  order.
  inversion_clear Hm'.
@@ -420,7 +420,7 @@ Proof.
  destruct (H0 x').
  assert (In x' ((x,e)::l)).
   apply H2; auto.
-  exists e'; auto.
+  exists e'...
  destruct (In_inv H3).
  order.
  inversion_clear Hm.
@@ -434,13 +434,13 @@ Proof.
  clear H1;destruct p as (k,e).
  destruct (H0 k).
  destruct H1.
- exists e; auto.
+ exists e...
  inversion H1.
 
  destruct p as (x,e).
  destruct (H0 x).
  destruct H.
- exists e; auto.
+ exists e...
  inversion H.
 
  destruct p;destruct p0;contradiction.
@@ -449,7 +449,7 @@ Qed.
 
 Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp,
   equal cmp m m' = true -> Equivb cmp m m'.
-Proof.
+Proof with auto with ordered_type.
  intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
  functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb;
   intuition; try discriminate; subst;
@@ -464,16 +464,16 @@ Proof.
  exists e'; constructor; split; trivial; apply X.eq_trans with x; auto.
  destruct (H k).
  destruct (H9 H8) as (e'',hyp).
- exists e''; auto.
+ exists e''...
 
  inversion_clear Hm;inversion_clear Hm'.
  destruct (andb_prop _ _ H); clear H.
  destruct (IHb H1 H3 H6).
  destruct (In_inv H0).
- exists e; constructor; split; trivial; apply X.eq_trans with x'; auto.
+ exists e; constructor; split; trivial; apply X.eq_trans with x'...
  destruct (H k).
  destruct (H10 H8) as (e'',hyp).
- exists e''; auto.
+ exists e''...
 
  inversion_clear Hm;inversion_clear Hm'.
  destruct (andb_prop _ _ H); clear H.
@@ -615,7 +615,8 @@ Proof.
  inversion_clear 1.
  exists x'.
  destruct H0; simpl in *.
- split; auto.
+ split.
+ auto with ordered_type.
  constructor 1.
  unfold eqke in *; simpl in *; intuition congruence.
  destruct IHm as (y, hyp); auto.
@@ -946,7 +947,7 @@ Proof.
  destruct (IHm0 H0) as (_,H4); apply H4; auto.
  case_eq (find x m0); intros; auto.
  assert (eqk (elt:=oee') (k,(oo,oo')) (x,(oo,oo'))).
-  red; auto.
+  red; auto with ordered_type.
  destruct (Sort_Inf_NotIn H0 (Inf_eq (eqk_sym H5) H1)).
  exists p; apply find_2; auto.
  (* k < x *)
@@ -1315,7 +1316,7 @@ Proof.
  apply (IHm1 H0 (Build_slist H5)); intuition.
 Qed.
 
-Ltac cmp_solve := unfold eq, lt; simpl; try Raw.MX.elim_comp; auto.
+Ltac cmp_solve := unfold eq, lt; simpl; try Raw.MX.elim_comp; auto with ordered_type.
 
 Definition compare : forall m1 m2, Compare lt eq m1 m2.
 Proof.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 6e08c38a49..f0b31e6986 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -63,11 +63,11 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
     {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}.
   Proof.
     intros; exists (remove x s); intuition.
-    absurd (In x (remove x s)); auto with set.
-    apply In_1 with y; auto.
+    absurd (In x (remove x s)); auto with set ordered_type.
+    apply In_1 with y; auto with ordered_type.
     elim (E.eq_dec x y); intros; auto.
-    absurd (In x (remove x s)); auto with set.
-    apply In_1 with y; auto.
+    absurd (In x (remove x s)); auto with set ordered_type.
+    apply In_1 with y; auto with ordered_type.
     eauto with set.
   Qed.
 
@@ -470,7 +470,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
   Hint Resolve elements_3 : core.
 
   Lemma elements_3w : forall s : t, NoDupA E.eq (elements s).
-  Proof. auto. Qed.
+  Proof. auto with ordered_type. Qed.
 
   Definition min_elt (s : t) : option elt :=
     match min_elt s with
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index c6b2e0a09d..e500debc73 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -939,7 +939,7 @@ Module OrdProperties (M:S).
    generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto.
    intros.
    symmetry; rewrite H1.
-   apply ME.eq_lt with a; auto.
+   apply ME.eq_lt with a; auto with ordered_type.
    rewrite <- H0; auto.
    intros.
    rewrite H0.
@@ -1013,7 +1013,7 @@ Module OrdProperties (M:S).
   intros.
   inversion_clear H2.
   rewrite <- elements_iff in H1.
-  apply ME.lt_eq with x; auto.
+  apply ME.lt_eq with x; auto with ordered_type.
   inversion H3.
   red; intros a.
   rewrite InA_app_iff, InA_cons, InA_nil by auto with *.
@@ -1052,7 +1052,7 @@ Module OrdProperties (M:S).
   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 ordered_type.
   inversion H0; auto.
   red; intros.
   rewrite remove_iff in H0; destruct H0.
@@ -1073,7 +1073,7 @@ Module OrdProperties (M:S).
   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 ordered_type.
   inversion H0; auto.
   red; intros.
   rewrite remove_iff in H0; destruct H0.