[stdlib] Remove a few `auto with *`

1 files changed, 22 insertions, 22 deletions

diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 88d12fc387..98b445580b 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -365,7 +365,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' ->
            P s' a -> P s'' (f x a)).
    intros; eapply Pstep; eauto.
-   rewrite elements_iff, <- InA_rev; auto with *.
+   rewrite elements_iff, <- InA_rev; auto.
   assert (Hdup : NoDup l) by
     (unfold l; eauto using elements_3w, NoDupA_rev with *).
   assert (Hsame : forall x, In x s <-> InA x l) by
@@ -435,7 +435,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   intros A B R f g i j s Rempty Rstep.
   rewrite 2 fold_spec_right. set (l:=rev (elements s)).
   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 *).
+    (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto).
   clearbody l; clear Rstep s.
   induction l; simpl; auto.
   Qed.
@@ -487,7 +487,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
         fold f s i = fold_right f i l.
   Proof.
   intros; exists (rev (elements s)); split.
-  apply NoDupA_rev; auto with *.
+  apply NoDupA_rev. auto with typeclass_instances. auto with set.
   split; intros.
   rewrite elements_iff; do 2 rewrite InA_alt.
   split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
@@ -521,7 +521,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2)));
     destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
   rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
-  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto with *.
+  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA). auto with typeclass_instances. 1-5: auto.
   rewrite <- Hl1; auto.
   intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1;
    rewrite (H2 a); intuition.
@@ -550,7 +550,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   intros.
   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 with *.
+  transitivity (f x0 (f x b)); auto. apply Comp; auto.
   Qed.
 
   (** ** Fold is a morphism *)
@@ -559,7 +559,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
    eqA (fold f s i) (fold f s i').
   Proof.
   intros. apply fold_rel with (R:=eqA); auto.
-   intros; apply Comp; auto with *.
+   intros; apply Comp; auto.
   Qed.
 
   Lemma fold_equal :
@@ -914,7 +914,7 @@ Module OrdProperties (M:S).
   Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
    sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
   Proof.
-  apply SortA_equivlistA_eqlistA; eauto with *.
+  apply SortA_equivlistA_eqlistA; auto with typeclass_instances.
   Qed.
 
   Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
@@ -958,7 +958,7 @@ Module OrdProperties (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 _ E.lt); auto with *.
+  eapply (@filter_split _ E.eq _ E.lt). 1-2: auto with typeclass_instances. 2: auto with set.
   intros.
   rewrite gtb_1 in H.
   assert (~E.lt y x).
@@ -972,32 +972,32 @@ Module OrdProperties (M:S).
   Proof.
   intros; unfold elements_ge, elements_lt.
   apply sort_equivlistA_eqlistA; auto with set.
-  apply (@SortA_app _ E.eq); auto with *.
-  apply (@filter_sort _ E.eq); auto with *.
+  apply (@SortA_app _ E.eq). auto with typeclass_instances.
+  apply (@filter_sort _ E.eq). 1-3: auto with typeclass_instances. auto with set.
   constructor; auto.
-  apply (@filter_sort _ E.eq); auto with *.
-  rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with *).
+  apply (@filter_sort _ E.eq). 1-3: auto with typeclass_instances. auto with set.
+  rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); auto with set typeclass_instances).
   intros.
-  rewrite filter_InA in H1; auto with *; destruct H1.
+  rewrite filter_InA in H1 by auto with fset. destruct H1.
   rewrite leb_1 in H2.
   rewrite <- elements_iff in H1.
   assert (~E.eq x y).
    contradict H; rewrite H; auto.
   ME.order.
   intros.
-  rewrite filter_InA in H1; auto with *; destruct H1.
+  rewrite filter_InA in H1 by auto with fset. destruct H1.
   rewrite gtb_1 in H3.
   inversion_clear H2.
   ME.order.
-  rewrite filter_InA in H4; auto with *; destruct H4.
+  rewrite filter_InA in H4 by auto with fset. destruct H4.
   rewrite leb_1 in H4.
   ME.order.
   red; intros a.
   rewrite InA_app_iff, InA_cons, !filter_InA, <-elements_iff,
-   leb_1, gtb_1, (H0 a) by auto with *.
+   leb_1, gtb_1, (H0 a) by auto with fset.
   intuition.
   destruct (E.compare a x); intuition.
-  fold (~E.lt a x); auto with *.
+  fold (~E.lt a x); auto with ordered_type set.
   Qed.
 
   Definition Above x s := forall y, In y s -> E.lt y x.
@@ -1008,15 +1008,15 @@ Module OrdProperties (M:S).
      eqlistA E.eq (elements s') (elements s ++ x::nil).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with *.
-  apply (@SortA_app _ E.eq); auto with *.
+  apply sort_equivlistA_eqlistA. auto with set.
+  apply (@SortA_app _ E.eq). auto with typeclass_instances. auto with set. auto.
   intros.
   inversion_clear H2.
   rewrite <- elements_iff in H1.
   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 *.
+  rewrite InA_app_iff, InA_cons, InA_nil.
   do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
   Qed.
 
@@ -1025,9 +1025,9 @@ Module OrdProperties (M:S).
      eqlistA E.eq (elements s') (x::elements s).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with *.
+  apply sort_equivlistA_eqlistA. auto with set.
   change (sort E.lt ((x::nil) ++ elements s)).
-  apply (@SortA_app _ E.eq); auto with *.
+  apply (@SortA_app _ E.eq). auto with typeclass_instances. auto. auto with set.
   intros.
   inversion_clear H1.
   rewrite <- elements_iff in H2.