From daad81ddd72f4a8892b683d4f2b72345ff0bb84f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 10 Mar 2020 13:02:15 +0100
Subject: [stdlib] Remove a few `auto with *`

---
 theories/FSets/FSetCompat.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'theories/FSets/FSetCompat.v')

diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index 4edeaee72e..bff999042b 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -381,22 +381,22 @@ Module Update_Sets
   Instance lt_strorder : StrictOrder lt.
   Proof.
    split.
-   intros x Hx. apply (M.lt_not_eq Hx); auto with *.
+   intros x Hx. apply (M.lt_not_eq Hx). auto with crelations.
    exact M.lt_trans.
   Qed.
 
   Instance lt_compat : Proper (eq==>eq==>iff) lt.
   Proof.
-  apply proper_sym_impl_iff_2; auto with *.
+  apply proper_sym_impl_iff_2. 1-2: auto with crelations.
   intros s s' Hs u u' Hu H.
   assert (H0 : lt s' u).
    destruct (M.compare s' u) as [H'|H'|H']; auto.
-   elim (M.lt_not_eq H). transitivity s'; auto with *.
+   elim (M.lt_not_eq H). transitivity s'; auto.
    elim (M.lt_not_eq (M.lt_trans H H')); auto.
   destruct (M.compare s' u') as [H'|H'|H']; auto.
   elim (M.lt_not_eq H).
-   transitivity u'; auto with *. transitivity s'; auto with *.
-  elim (M.lt_not_eq (M.lt_trans H' H0)); auto with *.
+   transitivity u'. 2: auto with crelations. transitivity s'; auto.
+  elim (M.lt_not_eq (M.lt_trans H' H0)); auto with crelations.
   Qed.
 
   Definition compare s s' :=
-- 
cgit v1.2.3