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/FMapPositive.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index e9cb0a6aa7..c3c6c96997 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -679,7 +679,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   simpl; auto.
   destruct o; simpl; intros.
   (* Some *)
-  apply (SortA_app (eqA:=eq_key_elt)); auto with *.
+  apply (SortA_app (eqA:=eq_key_elt)). 1-2: auto with typeclass_instances.
   constructor; auto.
   apply In_InfA; intros.
   destruct y0.
@@ -698,7 +698,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   eapply xelements_bits_lt_1; eauto.
   eapply xelements_bits_lt_2; eauto.
   (* None *)
-  apply (SortA_app (eqA:=eq_key_elt)); auto with *.
+  apply (SortA_app (eqA:=eq_key_elt)). auto with typeclass_instances. 1-2: auto.
   intros x0 y0.
   do 2 rewrite InA_alt.
   intros (y1,(Hy1,H)) (y2,(Hy2,H0)).
-- 
cgit v1.2.3