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/Classes/CMorphisms.v     | 2 +-
 theories/Classes/Morphisms.v      | 2 +-
 theories/Classes/Morphisms_Prop.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Classes')

diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index c247bc11dc..598bd8b9c5 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -638,7 +638,7 @@ Instance PartialOrder_proper_type `(PartialOrder A eqA R) :
   Proper (eqA==>eqA==>iffT) R.
 Proof.
 intros.
-apply proper_sym_arrow_iffT_2; auto with *.
+apply proper_sym_arrow_iffT_2. 1-2: auto with crelations.
 intros x x' Hx y y' Hy Hr.
 transitivity x.
 - generalize (partial_order_equivalence x x'); compute; intuition.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 5adb927357..43adb0b69f 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -640,7 +640,7 @@ Instance PartialOrder_proper `(PartialOrder A eqA R) :
   Proper (eqA==>eqA==>iff) R.
 Proof.
 intros.
-apply proper_sym_impl_iff_2; auto with *.
+apply proper_sym_impl_iff_2. 1-2: auto with relations.
 intros x x' Hx y y' Hy Hr.
 transitivity x.
 - generalize (partial_order_equivalence x x'); compute; intuition.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 418f7a8767..7d0382ec43 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -75,7 +75,7 @@ Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop)
  `(Equivalence _ E) `(Proper _ (E==>E==>iff) R) :
  Proper (E==>iff) (Acc R).
 Proof.
- apply proper_sym_impl_iff; auto with *.
+ apply proper_sym_impl_iff. auto with relations.
  intros x y EQ WF. apply Acc_intro; intros z Hz.
 rewrite <- EQ in Hz. now apply Acc_inv with x.
 Qed.
-- 
cgit v1.2.3