Cleanup attempt of Hints in *Interface.v files.

See recent discussion in coq-club.



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

11 files changed, 208 insertions, 194 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index b119f27ce..0906099de 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -114,9 +114,9 @@ intros.
 intuition.
 destruct (eq_dec x y); [left|right].
 split; auto.
-symmetry; apply (MapsTo_fun (e':=e) H); auto.
+symmetry; apply (MapsTo_fun (e':=e) H); auto with map.
 split; auto; apply add_3 with x e; auto.
-subst; auto.
+subst; auto with map.
 Qed.
 
 Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m.
@@ -204,27 +204,27 @@ split.
 case_eq (find x m); intros.
 exists e.
 split.
-apply (MapsTo_fun (m:=map f m) (x:=x)); auto.
-apply find_2; auto.
+apply (MapsTo_fun (m:=map f m) (x:=x)); auto with map.
+apply find_2; auto with map.
 assert (In x (map f m)) by (exists b; auto).
 destruct (map_2 H1) as (a,H2).
 rewrite (find_1 H2) in H; discriminate.
 intros (a,(H,H0)).
-subst b; auto.
+subst b; auto with map.
 Qed.
 
 Lemma map_in_iff : forall m x (f : elt -> elt'), 
  In x (map f m) <-> In x m.
 Proof.
-split; intros; eauto.
+split; intros; eauto with map.
 destruct H as (a,H).
-exists (f a); auto.
+exists (f a); auto with map.
 Qed.
 
 Lemma mapi_in_iff : forall m x (f:key->elt->elt'),
  In x (mapi f m) <-> In x m.
 Proof.
-split; intros; eauto.
+split; intros; eauto with map.
 destruct H as (a,H).
 destruct (mapi_1 f H) as (y,(H0,H1)).
 exists (f y a); auto.
@@ -240,9 +240,9 @@ Proof.
 intros; case_eq (find x m); intros.
 exists e.
 destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)).
-apply find_2; auto.
-exists y; repeat split; auto.
-apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto.
+apply find_2; auto with map.
+exists y; repeat split; auto with map.
+apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto with map.
 assert (In x (mapi f m)) by (exists b; auto).
 destruct (mapi_2 H1) as (a,H2).
 rewrite (find_1 H2) in H0; discriminate.
@@ -345,24 +345,24 @@ Qed.
 Lemma add_eq_o : forall m x y e, 
  E.eq x y -> find y (add x e m) = Some e.
 Proof.
-auto.
+auto with map.
 Qed.
 
 Lemma add_neq_o : forall m x y e, 
  ~ E.eq x y -> find y (add x e m) = find y m. 
 Proof.
 intros.
-case_eq (find y m); intros; auto.
-case_eq (find y (add x e m)); intros; auto.
+case_eq (find y m); intros; auto with map.
+case_eq (find y (add x e m)); intros; auto with map.
 rewrite <- H0; symmetry.
-apply find_1; apply add_3 with x e; auto.
+apply find_1; apply add_3 with x e; auto with map.
 Qed.
-Hint Resolve add_neq_o.
+Hint Resolve add_neq_o : map.
 
 Lemma add_o : forall m x y e, 
  find y (add x e m) = if eq_dec x y then Some e else find y m.
 Proof.
-intros; destruct (eq_dec x y); auto.
+intros; destruct (eq_dec x y); auto with map.
 Qed.
 
 Lemma add_eq_b : forall m x y e, 
@@ -394,23 +394,23 @@ destruct (find y (remove x m)); auto.
 destruct 2.
 exists e; rewrite H0; auto.
 Qed.
-Hint Resolve remove_eq_o.
+Hint Resolve remove_eq_o : map.
 
 Lemma remove_neq_o : forall m x y, 
  ~ E.eq x y -> find y (remove x m) = find y m. 
 Proof.
 intros.
-case_eq (find y m); intros; auto.
-case_eq (find y (remove x m)); intros; auto.
+case_eq (find y m); intros; auto with map.
+case_eq (find y (remove x m)); intros; auto with map.
 rewrite <- H0; symmetry.
-apply find_1; apply remove_3 with x; auto.
+apply find_1; apply remove_3 with x; auto with map.
 Qed.
-Hint Resolve remove_neq_o.
+Hint Resolve remove_neq_o : map.
 
 Lemma remove_o : forall m x y, 
  find y (remove x m) = if eq_dec x y then None else find y m.
 Proof.
-intros; destruct (eq_dec x y); auto.
+intros; destruct (eq_dec x y); auto with map.
 Qed.
 
 Lemma remove_eq_b : forall m x y, 
@@ -495,14 +495,14 @@ intros.
 case_eq (find x m); intros.
 rewrite <- H0.
 apply map2_1; auto.
-left; exists e; auto.
+left; exists e; auto with map.
 case_eq (find x m'); intros.
 rewrite <- H0; rewrite <- H1.
 apply map2_1; auto.
-right; exists e; auto.
+right; exists e; auto with map.
 rewrite H.
-case_eq (find x (map2 f m m')); intros; auto.
-assert (In x (map2 f m m')) by (exists e; auto).
+case_eq (find x (map2 f m m')); intros; auto with map.
+assert (In x (map2 f m m')) by (exists e; auto with map).
 destruct (map2_2 H3) as [(e0,H4)|(e0,H4)].
 rewrite (find_1 H4) in H0; discriminate.
 rewrite (find_1 H4) in H1; discriminate.
@@ -647,13 +647,13 @@ Module Properties (M: S).
    unfold leb; f_equal; apply gtb_compat; auto.
   Qed.
 
-  Hint Resolve gtb_compat leb_compat elements_3.
+  Hint Resolve gtb_compat leb_compat elements_3 : map.
 
   Lemma elements_split : forall p m, 
     elements m = elements_lt p m ++ elements_ge p m.
   Proof.
   unfold elements_lt, elements_ge, leb; intros.
-  apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto.
+  apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with map.
   intros; destruct x; destruct y; destruct p.
   rewrite gtb_1 in H; unfold O.ltk in H; simpl in *.
   assert (~ltk (t1,e0) (k,e1)).
@@ -667,15 +667,15 @@ Module Properties (M: S).
                  (elements_lt (x,e) m ++ (x,e):: elements_ge (x,e) m).
   Proof.
   intros; unfold elements_lt, elements_ge.
-  apply sort_equivlistA_eqlistA; auto.
-  apply (@SortA_app _ eqke); auto.
-  apply (@filter_sort _ eqke); auto; clean_eauto.
-  constructor; auto.
-  apply (@filter_sort _ eqke); auto; clean_eauto.
-  rewrite (@InfA_alt _ eqke); auto; try (clean_eauto; fail).
-  apply (@filter_sort _ eqke); auto; clean_eauto.
+  apply sort_equivlistA_eqlistA; auto with map.
+  apply (@SortA_app _ eqke); auto with map.
+  apply (@filter_sort _ eqke); auto with map; clean_eauto.
+  constructor; auto with map.
+  apply (@filter_sort _ eqke); auto with map; clean_eauto.
+  rewrite (@InfA_alt _ eqke); auto with map; try (clean_eauto; fail).
+  apply (@filter_sort _ eqke); auto with map; clean_eauto.
   intros.
-  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite filter_InA in H1; auto with map; destruct H1.
   rewrite leb_1 in H2.
   destruct y; unfold O.ltk in *; simpl in *.
   rewrite <- elements_mapsto_iff in H1.
@@ -684,18 +684,18 @@ Module Properties (M: S).
    exists e0; apply MapsTo_1 with t0; auto.
   ME.order.
   intros.
-  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite filter_InA in H1; auto with map; destruct H1.
   rewrite gtb_1 in H3.
   destruct y; destruct x0; unfold O.ltk in *; simpl in *.
   inversion_clear H2.
   red in H4; simpl in *; destruct H4.
   ME.order.
-  rewrite filter_InA in H4; auto; destruct H4.
+  rewrite filter_InA in H4; auto with map; destruct H4.
   rewrite leb_1 in H4.
   unfold O.ltk in *; simpl in *; ME.order.
   red; intros a; destruct a.
   rewrite InA_app_iff; rewrite InA_cons.
-  do 2 (rewrite filter_InA; auto).
+  do 2 (rewrite filter_InA; auto with map).
   do 2 rewrite <- elements_mapsto_iff.
   rewrite leb_1; rewrite gtb_1.
   rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
@@ -716,8 +716,8 @@ Module Properties (M: S).
      eqlistA eqke (elements m') (elements m ++ (x,e)::nil).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto.
-  apply (@SortA_app _ eqke); auto.
+  apply sort_equivlistA_eqlistA; auto with map.
+  apply (@SortA_app _ eqke); auto with map.
   intros.
   inversion_clear H2.
   destruct x0; destruct y.
@@ -745,9 +745,9 @@ Module Properties (M: S).
      eqlistA eqke (elements m') ((x,e)::elements m).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto.
+  apply sort_equivlistA_eqlistA; auto with map.
   change (sort ltk (((x,e)::nil) ++ elements m)).
-  apply (@SortA_app _ eqke); auto.
+  apply (@SortA_app _ eqke); auto with map.
   intros.
   inversion_clear H1.
   destruct y; destruct x0.
@@ -774,7 +774,7 @@ Module Properties (M: S).
    Equal m m' -> eqlistA eqke (elements m) (elements m').
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto.
+  apply sort_equivlistA_eqlistA; auto with map.
   red; intros.
   destruct x; do 2 rewrite <- elements_mapsto_iff.
   do 2 rewrite find_mapsto_iff; rewrite H; split; auto.
@@ -978,12 +978,12 @@ Module Properties (M: S).
   destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *.
   assert (Add x e (remove x m) m).
    red; intros.
-   rewrite add_o; rewrite remove_o; destruct (ME.eq_dec x y); eauto.
-  apply X0 with (remove x m) x e; auto.
-  apply IHn; auto.
+   rewrite add_o; rewrite remove_o; destruct (ME.eq_dec x y); eauto with map.
+  apply X0 with (remove x m) x e; auto with map.
+  apply IHn; auto with map.
   assert (S n = S (cardinal (remove x m))).
-   rewrite Heqn; eapply cardinal_2; eauto.
-  inversion H1; auto.
+   rewrite Heqn; eapply cardinal_2; eauto with map.
+  inversion H1; auto with map.
   Qed.
 
   Lemma map_induction_max :
@@ -1002,11 +1002,11 @@ Module Properties (M: S).
    rewrite add_o; rewrite remove_o; destruct (ME.eq_dec k y); eauto.
    apply find_1; apply MapsTo_1 with k; auto.
    apply max_elt_MapsTo; auto.
-  apply X0 with (remove k m) k e; auto.
+  apply X0 with (remove k m) k e; auto with map.
   apply IHn.
   assert (S n = S (cardinal (remove k m))).
    rewrite Heqn.
-   eapply cardinal_2; eauto.
+   eapply cardinal_2; eauto with map.
   inversion H1; auto. 
   eapply max_elt_Above; eauto.
 
@@ -1033,7 +1033,7 @@ Module Properties (M: S).
   apply IHn.
   assert (S n = S (cardinal (remove k m))).
    rewrite Heqn.
-   eapply cardinal_2; eauto.
+   eapply cardinal_2; eauto with map.
   inversion H1; auto. 
   eapply min_elt_Below; eauto.
 
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 0bd2c4525..d4e07461c 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -12,12 +12,9 @@
 
 (** This file proposes an interface for finite maps *)
 
-(* begin hide *)
-Require Export Bool.
-Require Export OrderedType.
+Require Export Bool OrderedType.
 Set Implicit Arguments.
 Unset Strict Implicit.
-(* end hide *)
 
 (** When compared with Ocaml Map, this signature has been split in two: 
    - The first part [S] contains the usual operators (add, find, ...)
@@ -206,12 +203,14 @@ Module Type S.
 	(x:key)(f:option elt->option elt'->option elt''), 
         In x (map2 f m m') -> In x m \/ In x m'.
 
-  (* begin hide *)
-  Hint Immediate MapsTo_1 mem_2 is_empty_2.
-  
-  Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 add_3 remove_1
-    remove_2 remove_3 find_1 find_2 fold_1 map_1 map_2 mapi_1 mapi_2. 
-  (* end hide *)
+  Hint Immediate MapsTo_1 mem_2 is_empty_2 
+    map_2 mapi_2 add_3 remove_3 find_2
+    : map.
+  Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
+    remove_2 find_1 fold_1 map_1 mapi_1 mapi_2
+    : map.
+  (** for compatibility with earlier hints *)
+  Hint Resolve map_2 mapi_2 add_3 remove_3 find_2 : oldmap.
 
 End S.
 
diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index 180df008e..e0f5e1c93 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -112,9 +112,9 @@ intros.
 intuition.
 destruct (E.eq_dec x y); [left|right].
 split; auto.
-symmetry; apply (MapsTo_fun (e':=e) H); auto.
+symmetry; apply (MapsTo_fun (e':=e) H); auto with map.
 split; auto; apply add_3 with x e; auto.
-subst; auto.
+subst; auto with map.
 Qed.
 
 Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m.
@@ -202,27 +202,27 @@ split.
 case_eq (find x m); intros.
 exists e.
 split.
-apply (MapsTo_fun (m:=map f m) (x:=x)); auto.
-apply find_2; auto.
+apply (MapsTo_fun (m:=map f m) (x:=x)); auto with map.
+apply find_2; auto with map.
 assert (In x (map f m)) by (exists b; auto).
 destruct (map_2 H1) as (a,H2).
 rewrite (find_1 H2) in H; discriminate.
 intros (a,(H,H0)).
-subst b; auto.
+subst b; auto with map.
 Qed.
 
 Lemma map_in_iff : forall m x (f : elt -> elt'), 
  In x (map f m) <-> In x m.
 Proof.
-split; intros; eauto.
+split; intros; eauto with map.
 destruct H as (a,H).
-exists (f a); auto.
+exists (f a); auto with map.
 Qed.
 
 Lemma mapi_in_iff : forall m x (f:key->elt->elt'),
  In x (mapi f m) <-> In x m.
 Proof.
-split; intros; eauto.
+split; intros; eauto with map.
 destruct H as (a,H).
 destruct (mapi_1 f H) as (y,(H0,H1)).
 exists (f y a); auto.
@@ -238,9 +238,9 @@ Proof.
 intros; case_eq (find x m); intros.
 exists e.
 destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)).
-apply find_2; auto.
-exists y; repeat split; auto.
-apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto.
+apply find_2; auto with map.
+exists y; repeat split; auto with map.
+apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto with map.
 assert (In x (mapi f m)) by (exists b; auto).
 destruct (mapi_2 H1) as (a,H2).
 rewrite (find_1 H2) in H0; discriminate.
@@ -345,24 +345,24 @@ Qed.
 Lemma add_eq_o : forall m x y e, 
  E.eq x y -> find y (add x e m) = Some e.
 Proof.
-auto.
+auto with map.
 Qed.
 
 Lemma add_neq_o : forall m x y e, 
  ~ E.eq x y -> find y (add x e m) = find y m. 
 Proof.
 intros.
-case_eq (find y m); intros; auto.
-case_eq (find y (add x e m)); intros; auto.
+case_eq (find y m); intros; auto with map.
+case_eq (find y (add x e m)); intros; auto with map.
 rewrite <- H0; symmetry.
-apply find_1; apply add_3 with x e; auto.
+apply find_1; apply add_3 with x e; auto with map.
 Qed.
-Hint Resolve add_neq_o.
+Hint Resolve add_neq_o : map.
 
 Lemma add_o : forall m x y e, 
  find y (add x e m) = if E.eq_dec x y then Some e else find y m.
 Proof.
-intros; destruct (E.eq_dec x y); auto.
+intros; destruct (E.eq_dec x y); auto with map.
 Qed.
 
 Lemma add_eq_b : forall m x y e, 
@@ -394,23 +394,23 @@ destruct (find y (remove x m)); auto.
 destruct 2.
 exists e; rewrite H0; auto.
 Qed.
-Hint Resolve remove_eq_o.
+Hint Resolve remove_eq_o : map.
 
 Lemma remove_neq_o : forall m x y, 
  ~ E.eq x y -> find y (remove x m) = find y m. 
 Proof.
 intros.
-case_eq (find y m); intros; auto.
-case_eq (find y (remove x m)); intros; auto.
+case_eq (find y m); intros; auto with map.
+case_eq (find y (remove x m)); intros; auto with map.
 rewrite <- H0; symmetry.
-apply find_1; apply remove_3 with x; auto.
+apply find_1; apply remove_3 with x; auto with map.
 Qed.
-Hint Resolve remove_neq_o.
+Hint Resolve remove_neq_o : map.
 
 Lemma remove_o : forall m x y, 
  find y (remove x m) = if E.eq_dec x y then None else find y m.
 Proof.
-intros; destruct (E.eq_dec x y); auto.
+intros; destruct (E.eq_dec x y); auto with map.
 Qed.
 
 Lemma remove_eq_b : forall m x y, 
@@ -494,15 +494,15 @@ Proof.
 intros.
 case_eq (find x m); intros.
 rewrite <- H0.
-apply map2_1; auto.
-left; exists e; auto.
+apply map2_1; auto with map.
+left; exists e; auto with map.
 case_eq (find x m'); intros.
 rewrite <- H0; rewrite <- H1.
 apply map2_1; auto.
-right; exists e; auto.
+right; exists e; auto with map.
 rewrite H.
-case_eq (find x (map2 f m m')); intros; auto.
-assert (In x (map2 f m m')) by (exists e; auto).
+case_eq (find x (map2 f m m')); intros; auto with map.
+assert (In x (map2 f m m')) by (exists e; auto with map).
 destruct (map2_2 H3) as [(e0,H4)|(e0,H4)].
 rewrite (find_1 H4) in H0; discriminate.
 rewrite (find_1 H4) in H1; discriminate.
@@ -667,7 +667,7 @@ Module Properties (M: S).
   inversion H3; auto.
   f_equal; auto.
   elim H1.
-  exists b; apply MapsTo_1 with a; auto.
+  exists b; apply MapsTo_1 with a; auto with map.
   elim n; auto.
   Qed.
 
@@ -710,7 +710,7 @@ Module Properties (M: S).
   red; inversion 1.
   inversion H.
   Qed.
-  Hint Resolve cardinal_inv_1.
+  Hint Resolve cardinal_inv_1 : map.
 
   Lemma cardinal_inv_2 :
    forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
@@ -735,12 +735,12 @@ Module Properties (M: S).
   destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *.
   assert (Add x e (remove x m) m).
    red; intros.
-   rewrite add_o; rewrite remove_o; destruct (E.eq_dec x y); eauto.
-  apply X0 with (remove x m) x e; auto.
-  apply IHn; auto.
+   rewrite add_o; rewrite remove_o; destruct (E.eq_dec x y); eauto with map.
+  apply X0 with (remove x m) x e; auto with map.
+  apply IHn; auto with map.
   assert (S n = S (cardinal (remove x m))).
-   rewrite Heqn; eapply cardinal_2; eauto.
-  inversion H1; auto.
+   rewrite Heqn; eapply cardinal_2; eauto with map.
+  inversion H1; auto with map.
   Qed.
 
  End Elt.
diff --git a/theories/FSets/FMapWeakInterface.v b/theories/FSets/FMapWeakInterface.v
index 5a9d3cca6..c4bfad59a 100644
--- a/theories/FSets/FMapWeakInterface.v
+++ b/theories/FSets/FMapWeakInterface.v
@@ -13,12 +13,9 @@
 (** This file proposes an interface for finite maps over keys with decidable 
      equality, but no decidable order. *)
 
-(* begin hide *)
-Require Export Bool.
-Require Export DecidableType.
+Require Export Bool DecidableType.
 Set Implicit Arguments.
 Unset Strict Implicit.
-(* end hide *)
 
 Module Type S.
 
@@ -195,9 +192,13 @@ Module Type S.
 	(x:key)(f:option elt->option elt'->option elt''), 
         In x (map2 f m m') -> In x m \/ In x m'.
 
-  Hint Immediate MapsTo_1 mem_2 is_empty_2.
-  
-  Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 add_3 remove_1
-    remove_2 remove_3 find_1 find_2 fold_1 map_1 map_2 mapi_1 mapi_2. 
+  Hint Immediate MapsTo_1 mem_2 is_empty_2
+    map_2 mapi_2 add_3 remove_3 find_2
+    : map.
+  Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
+    remove_2 find_1 fold_1 map_1 mapi_1 mapi_2
+    : map.
+  (** for compatibility with earlier hints *)
+  Hint Resolve map_2 mapi_2 add_3 remove_3 find_2 : oldmap.
 
 End S.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 55b00f063..c5656402f 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -27,7 +27,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
    
   Definition empty : {s : t | Empty s}.
   Proof. 
-    exists empty; auto.
+    exists empty; auto with set.
   Qed.
 
   Definition is_empty : forall s : t, {Empty s} + {~ Empty s}.
@@ -66,12 +66,12 @@ Module DepOfNodep (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.
+    absurd (In x (remove x s)); auto with set.
     apply In_1 with y; auto. 
     elim (ME.eq_dec x y); intros; auto.
-    absurd (In x (remove x s)); auto.
+    absurd (In x (remove x s)); auto with set.
     apply In_1 with y; auto. 
-    eauto.
+    eauto with set.
   Qed.
 
   Definition union :
@@ -83,14 +83,14 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
   Definition inter :
     forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ In x s'}.
   Proof. 
-    intros; exists (inter s s'); intuition; eauto.
+    intros; exists (inter s s'); intuition; eauto with set.
   Qed.
 
   Definition diff :
     forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ ~ In x s'}.
   Proof. 
-    intros; exists (diff s s'); intuition; eauto. 
-    absurd (In x s'); eauto. 
+    intros; exists (diff s s'); intuition; eauto with set. 
+    absurd (In x s'); eauto with set. 
   Qed. 
  
   Definition equal : forall s s' : t, {Equal s s'} + {~ Equal s s'}.
@@ -150,7 +150,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
     exists (filter (fdec Pdec) s).
     intro H; assert (compat_bool E.eq (fdec Pdec)); auto.
     intuition.
-    eauto.
+    eauto with set.
     generalize (filter_2 H0 H1).
     unfold fdec in |- *.
     case (Pdec x); intuition.
@@ -226,7 +226,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
     generalize H4; unfold For_all, Equal in |- *; intuition.
     elim (H0 x); intros.
     assert (fdec Pdec x = true).
-     eauto.      
+     eapply filter_2; eauto with set.
     generalize H8; unfold fdec in |- *; case (Pdec x); intuition.
     inversion H9.
     generalize H; unfold For_all, Equal in |- *; intuition.
@@ -238,8 +238,8 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
     set (b := fdec Pdec x) in *; generalize (refl_equal b);
      pattern b at -1 in |- *; case b; unfold b in |- *; 
      [ left | right ].
-    elim (H4 x); intros _ B; apply B; auto.
-    elim (H x); intros _ B; apply B; auto.
+    elim (H4 x); intros _ B; apply B; auto with set.
+    elim (H x); intros _ B; apply B; auto with set.
     apply filter_3; auto.
     rewrite H5; auto.
     eapply (filter_1 (s:=s) (x:=x) H2); elim (H4 x); intros B _; apply B;
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 9e1ca4058..4a99a44a3 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -76,7 +76,7 @@ Qed.
   
 Lemma empty_mem: mem x empty=false.
 Proof. 
-rewrite <- not_mem_iff; auto.
+rewrite <- not_mem_iff; auto with set.
 Qed.
 
 Lemma is_empty_equal_empty: is_empty s = equal s empty.
@@ -88,17 +88,17 @@ Qed.
   
 Lemma choose_mem_1: choose s=Some x -> mem x s=true.
 Proof.  
-auto.
+auto with set.
 Qed.
 
 Lemma choose_mem_2: choose s=None -> is_empty s=true.
 Proof.
-auto.
+auto with set.
 Qed.
 
 Lemma add_mem_1: mem x (add x s)=true.
 Proof.
-auto.
+auto with set.
 Qed.  
  
 Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
@@ -108,7 +108,7 @@ Qed.
 
 Lemma remove_mem_1: mem x (remove x s)=false.
 Proof. 
-rewrite <- not_mem_iff; auto.
+rewrite <- not_mem_iff; auto with set.
 Qed. 
  
 Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
@@ -216,7 +216,7 @@ Proof.
 intros.
 generalize (@choose_1 s) (@choose_2 s).
 destruct (choose s);intros.
-exists e;auto.
+exists e;auto with set.
 generalize (H1 (refl_equal None)); clear H1.
 intros; rewrite (is_empty_1 H1) in H; discriminate.
 Qed.
@@ -233,7 +233,7 @@ Qed.
 Lemma add_mem_3: 
  mem y s=true -> mem y (add x s)=true.
 Proof.
-auto.
+auto with set.
 Qed.
 
 Lemma add_equal: 
@@ -260,7 +260,7 @@ Qed.
 Lemma add_remove: 
  mem x s=true -> equal (add x (remove x s)) s=true.
 Proof.
-intros; apply equal_1; apply add_remove; auto.
+intros; apply equal_1; apply add_remove; auto with set.
 Qed.
 
 Lemma remove_add: 
@@ -275,9 +275,9 @@ Qed.
 Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
 Proof.
 intros; apply bool_1; split; intros.
-rewrite cardinal_1; simpl; auto.
+rewrite cardinal_1; simpl; auto with set.
 assert (cardinal s = 0) by (apply zerob_true_elim; auto).
-auto.
+auto with set.
 Qed.
 
 (** Properties of [singleton] *)
@@ -295,7 +295,7 @@ Qed.
 
 Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
 Proof.
-auto.
+intros; apply singleton_1; auto with set.
 Qed.
 
 (** Properties of [union] *)
@@ -358,7 +358,7 @@ Lemma union_subset_3:
  subset s s''=true -> subset s' s''=true -> 
   subset (union s s') s''=true.
 Proof.
-intros; apply subset_1; apply union_subset_3; auto.
+intros; apply subset_1; apply union_subset_3; auto with set.
 Qed.
 
 (** Properties of [inter] *) 
@@ -433,7 +433,7 @@ Lemma inter_subset_3:
  subset s'' s=true -> subset s'' s'=true -> 
   subset s'' (inter s s')=true.
 Proof.
-intros; apply subset_1; apply inter_subset_3; auto.
+intros; apply subset_1; apply inter_subset_3; auto with set.
 Qed.
 
 (** Properties of [diff] *)
@@ -516,7 +516,7 @@ Qed.
 Lemma fold_equal: 
  equal s s'=true -> eqA (fold f s i) (fold f s' i).
 Proof. 
-intros; apply fold_equal with (eqA:=eqA); auto.
+intros; apply fold_equal with (eqA:=eqA); auto with set.
 Qed.
    
 Lemma fold_add: 
@@ -529,13 +529,13 @@ Qed.
 Lemma add_fold: 
   mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
 Proof.
-intros; apply add_fold with (eqA:=eqA); auto.
+intros; apply add_fold with (eqA:=eqA); auto with set.
 Qed.
 
 Lemma remove_fold_1: 
  mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
 Proof.
-intros; apply remove_fold_1 with (eqA:=eqA); auto.
+intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
 Qed.
 
 Lemma remove_fold_2: 
@@ -573,13 +573,13 @@ Qed.
 Lemma remove_cardinal_1: 
  forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
 Proof.
-intros; apply remove_cardinal_1; auto.
+intros; apply remove_cardinal_1; auto with set.
 Qed.
 
 Lemma remove_cardinal_2: 
  forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
 Proof.
-auto with set.
+intros; apply Equal_cardinal; apply equal_2; auto with set.
 Qed.
 
 Lemma union_cardinal: 
@@ -593,7 +593,7 @@ Qed.
 Lemma subset_cardinal: 
  forall s s', subset s s'=true -> cardinal s<=cardinal s'.
 Proof.
-intros; apply subset_cardinal; auto.
+intros; apply subset_cardinal; auto with set.
 Qed.
 
 Section Bool.
@@ -636,7 +636,7 @@ Proof.
 intros; apply bool_1; split; intros. 
 destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).
 apply bool_6.
-red; intros; apply (@is_empty_2 _ H0 a); auto.
+red; intros; apply (@is_empty_2 _ H0 a); auto with set.
 generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)).
 destruct (choose (filter f s)).
 intros H0 _; apply exists_1; auto.
@@ -648,13 +648,13 @@ Qed.
 Lemma partition_filter_1: 
  forall s, equal (fst (partition f s)) (filter f s)=true.
 Proof. 
-auto.
+auto with set.
 Qed.
 
 Lemma partition_filter_2: 
  forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
 Proof. 
-auto.
+auto with set.
 Qed.
 
 Lemma filter_add_1 : forall s x, f x = true -> 
@@ -912,13 +912,13 @@ trans_st (fold f s0 i).
 apply fold_equal with (eqA:=eqA); auto.
 rewrite equal_sym; auto.
 trans_st (fold g s0 i).
-apply H0; intros; apply H1; auto.
-elim  (equal_2 H x); auto; intros.
-apply fold_equal with (eqA:=eqA); auto.
+apply H0; intros; apply H1; auto with set.
+elim  (equal_2 H x); auto with set; intros.
+apply fold_equal with (eqA:=eqA); auto with set.
 trans_st (f x (fold f s0 i)).
-apply fold_add with (eqA:=eqA); auto.
-trans_st (g x (fold f s0 i)).
-trans_st (g x (fold g s0 i)).
+apply fold_add with (eqA:=eqA); auto with set.
+trans_st (g x (fold f s0 i)); auto with set.
+trans_st (g x (fold g s0 i)); auto with set.
 sym_st; apply fold_add with (eqA:=eqA); auto.
 trans_st i; [idtac | sym_st ]; apply fold_empty; auto.
 Qed.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index ac0227f5c..e83b861fb 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -258,7 +258,8 @@ apply H0; auto.
 symmetry.
 rewrite H0; intros.
 destruct H1 as (_,H1).
-apply H1; auto.
+apply H1; auto with set.
+apply elements_2; auto with set.
 Qed.
 
 Lemma exists_b : compat_bool E.eq f -> 
@@ -271,7 +272,7 @@ destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros.
 rewrite <- H1; intros.
 destruct H0 as (H0,_).
 destruct H0 as (a,(Ha1,Ha2)); auto.
-exists a; auto.
+exists a; intuition; auto with set.
 symmetry.
 rewrite H0.
 destruct H1 as (_,H1).
@@ -420,7 +421,7 @@ Add Relation t Subset
 
 Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m.
 Proof.
-unfold Subset, impl; intros; eauto.
+unfold Subset, impl; intros; eauto with set.
 Qed.
 
 Add Morphism Empty with signature Subset --> impl as Empty_s_m.
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 012f95d87..ded81426d 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -12,12 +12,9 @@
 
 (** Set interfaces *)
 
-(* begin hide *)
-Require Export Bool.
-Require Export OrderedType.
+Require Export Bool OrderedType.
 Set Implicit Arguments.
 Unset Strict Implicit.
-(* end hide *)
 
 (** * Non-dependent signature
 
@@ -273,16 +270,25 @@ Module Type S.
 
   End Spec.
 
-  (* begin hide *)
-  Hint Immediate In_1.
+  Hint Resolve mem_1 equal_1 subset_1 empty_1
+    is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
+    remove_2 singleton_2 union_1 union_2 union_3
+    inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
+    partition_1 partition_2 elements_1 elements_3
+    : set.
+  Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
+    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
+    filter_1 filter_2 for_all_2 exists_2 elements_2
+    min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3
+    : set.
+  (** for compatibility with earlier hints *)
+  Hint Resolve mem_2 equal_2 subset_2 is_empty_2 add_3
+    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
+    filter_1 filter_2 for_all_2 exists_2 elements_2
+    min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3
+    : oldset.
   
-  Hint Resolve mem_1 mem_2 equal_1 equal_2 subset_1 subset_2 empty_1
-    is_empty_1 is_empty_2 choose_1 choose_2 add_1 add_2 add_3 remove_1
-    remove_2 remove_3 singleton_1 singleton_2 union_1 union_2 union_3 inter_1
-    inter_2 inter_3 diff_1 diff_2 diff_3 filter_1 filter_2 filter_3 for_all_1
-    for_all_2 exists_1 exists_2 partition_1 partition_2 elements_1 elements_2
-    elements_3 min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3.
-  (* end hide *)
+ 
 
 End S.
 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 2070cf815..d6c978c05 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -239,7 +239,7 @@ Module Properties (M: S).
   Proof.
   unfold Equal; intros; set_iff.
   destruct (ME.eq_dec x a); intuition.
-  left; eauto.
+  left; eauto with set.
   Qed.
 
   Lemma union_subset_1 : s [<=] union s s'.
@@ -525,7 +525,7 @@ Module Properties (M: S).
    elements s = elements_lt x s ++ elements_ge x s.
   Proof.
   unfold elements_lt, elements_ge, leb; intros.
-  eapply (@filter_split _ E.eq); eauto. ME.order. ME.order. ME.order.
+  eapply (@filter_split _ E.eq); eauto with set. ME.order. ME.order. ME.order.
   intros.
   rewrite gtb_1 in H.
   assert (~E.lt y x).
@@ -537,13 +537,13 @@ Module Properties (M: S).
     eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s). 
   Proof.
   intros; unfold elements_ge, elements_lt.
-  apply sort_equivlistA_eqlistA; auto.
+  apply sort_equivlistA_eqlistA; auto with set.
   apply (@SortA_app _ E.eq); auto.
-  apply (@filter_sort _ E.eq); auto; eauto.
+  apply (@filter_sort _ E.eq); auto with set; eauto with set.
   constructor; auto.
-  apply (@filter_sort _ E.eq); auto; eauto.
+  apply (@filter_sort _ E.eq); auto with set; eauto with set.
   rewrite Inf_alt; auto; intros.
-  apply (@filter_sort _ E.eq); auto; eauto.
+  apply (@filter_sort _ E.eq); auto with set; eauto with set.
   rewrite filter_InA in H1; auto; destruct H1.
   rewrite leb_1 in H2.
   rewrite <- elements_iff in H1.
@@ -574,8 +574,8 @@ Module Properties (M: S).
      eqlistA E.eq (elements s') (elements s ++ x::nil).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto.
-  apply (@SortA_app _ E.eq); auto.
+  apply sort_equivlistA_eqlistA; auto with set.
+  apply (@SortA_app _ E.eq); auto with set.
   intros.
   inversion_clear H2.
   rewrite <- elements_iff in H1.
@@ -591,9 +591,9 @@ Module Properties (M: S).
      eqlistA E.eq (elements s') (x::elements s).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto.
+  apply sort_equivlistA_eqlistA; auto with set.
   change (sort E.lt ((x::nil) ++ elements s)).
-  apply (@SortA_app _ E.eq); auto.
+  apply (@SortA_app _ E.eq); auto with set.
   intros.
   inversion_clear H1.
   rewrite <- elements_iff in H2.
@@ -615,7 +615,7 @@ Module Properties (M: S).
   intros.
   do 2 rewrite M.cardinal_1.
   apply (@eqlistA_length _ E.eq); auto.
-  apply sort_equivlistA_eqlistA; auto.
+  apply sort_equivlistA_eqlistA; auto with set.
   red; intro a.
   do 2 rewrite <- elements_iff; auto.
   Qed.
@@ -755,7 +755,7 @@ Module Properties (M: S).
         fold f s i = fold_right f i l.
   Proof.
   intros; exists (rev (elements s)); split.
-  apply NoDupA_rev; auto.
+  apply NoDupA_rev; auto with set.
   exact E.eq_trans.
   split; intros.
   rewrite elements_iff; do 2 rewrite InA_alt.
@@ -843,7 +843,7 @@ Module Properties (M: S).
 
   Lemma fold_empty : forall i, eqA (fold f empty i) i.
   Proof. 
-  intros; apply fold_1; auto.
+  intros; apply fold_1; auto with set.
   Qed.
 
   Lemma fold_equal : 
@@ -853,7 +853,7 @@ Module Properties (M: S).
   do 2 rewrite <- fold_left_rev_right.
   apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
   apply eqlistA_rev.
-  apply sort_equivlistA_eqlistA; auto.
+  apply sort_equivlistA_eqlistA; auto with set.
   red; intro a; do 2 rewrite <- elements_iff; auto.
   Qed.
 
@@ -882,7 +882,7 @@ Module Properties (M: S).
   Proof.
   intros.
   sym_st.
-  apply fold_2 with (eqA:=eqA); auto.
+  apply fold_2 with (eqA:=eqA); auto with set.
   Qed.
 
   Lemma remove_fold_2: forall i s x, ~In x s -> 
@@ -983,7 +983,7 @@ Module Properties (M: S).
 
   Lemma empty_cardinal : cardinal empty = 0.
   Proof.
-  rewrite cardinal_fold; apply fold_1; auto.
+  rewrite cardinal_fold; apply fold_1; auto with set.
   Qed.
 
   Hint Immediate empty_cardinal cardinal_1 : set.
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
index 72084d034..3079ec871 100644
--- a/theories/FSets/FSetWeakInterface.v
+++ b/theories/FSets/FSetWeakInterface.v
@@ -12,8 +12,7 @@
 
 (** Set interfaces for types with only a decidable equality, but no ordering *)
 
-Require Export Bool.
-Require Export DecidableType.
+Require Export Bool DecidableType.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -229,13 +228,21 @@ Module Type S.
 
   End Spec.
 
-  Hint Immediate In_1.
-  
-  Hint Resolve mem_1 mem_2 equal_1 equal_2 subset_1 subset_2 empty_1
-    is_empty_1 is_empty_2 choose_1 choose_2 add_1 add_2 add_3 remove_1
-    remove_2 remove_3 singleton_1 singleton_2 union_1 union_2 union_3 inter_1
-    inter_2 inter_3 diff_1 diff_2 diff_3 filter_1 filter_2 filter_3 for_all_1
-    for_all_2 exists_1 exists_2 partition_1 partition_2 elements_1 elements_2
-    elements_3.
+  Hint Resolve mem_1 equal_1 subset_1 empty_1
+    is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
+    remove_2 singleton_2 union_1 union_2 union_3
+    inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
+    partition_1 partition_2 elements_1 elements_3 
+    : set.
+  Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
+    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
+    filter_1 filter_2 for_all_2 exists_2 elements_2 
+    : set.
+  (* for compatibility with earlier hints *)
+  Hint Resolve In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
+    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
+    filter_1 filter_2 for_all_2 exists_2 elements_2 
+    : oldset.
+
 
 End S.
diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v
index 169543e32..07e087241 100644
--- a/theories/FSets/FSetWeakProperties.v
+++ b/theories/FSets/FSetWeakProperties.v
@@ -455,7 +455,7 @@ Module Properties (M: S).
         fold f s i = fold_right f i l.
   Proof.
   intros; exists (rev (elements s)); split.
-  apply NoDupA_rev; auto.
+  apply NoDupA_rev; auto with set.
   exact E.eq_trans.
   split; intros.
   rewrite elements_iff; do 2 rewrite InA_alt.
@@ -583,9 +583,9 @@ Module Properties (M: S).
   Proof.
   simple induction n; intros; auto.
   destruct (cardinal_inv_2 H) as (x,H0). 
-  apply X0 with (remove x s) x; auto.
-  apply X1; auto.
-  rewrite (cardinal_2 (x:=x)(s:=remove x s)(s':=s)) in H; auto.
+  apply X0 with (remove x s) x; auto with set.
+  apply X1; auto with set.
+  rewrite (cardinal_2 (x:=x)(s:=remove x s)(s':=s)) in H; auto with set.
   Qed.
 
   Lemma set_induction :
@@ -608,7 +608,7 @@ Module Properties (M: S).
 
   Lemma fold_empty : eqA (fold f empty i) i.
   Proof. 
-  apply fold_1; auto.
+  apply fold_1; auto with set.
   Qed.
 
   Lemma fold_equal : 
@@ -643,7 +643,7 @@ Module Properties (M: S).
   Proof.
   intros.
   sym_st.
-  apply fold_2 with (eqA:=eqA); auto.
+  apply fold_2 with (eqA:=eqA); auto with set.
   Qed.
 
   Lemma remove_fold_2: forall s x, ~In x s -> 
@@ -779,7 +779,7 @@ Module Properties (M: S).
 
   Lemma empty_cardinal : cardinal empty = 0.
   Proof.
-  rewrite cardinal_fold; apply fold_1; auto.
+  rewrite cardinal_fold; apply fold_1; auto with set.
   Qed.
 
   Hint Immediate empty_cardinal cardinal_1 : set.