diff options
| author | Vincent Laporte | 2020-03-10 13:02:15 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2020-03-19 08:05:02 +0100 |
| commit | daad81ddd72f4a8892b683d4f2b72345ff0bb84f (patch) | |
| tree | f757fb85c150ba2de7eb293e59c2158c8f4fc3b0 /theories/Classes | |
| parent | a1315d78a5b3c6095848298f03ca328380a7d453 (diff) | |
[stdlib] Remove a few `auto with *`
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/CMorphisms.v | 2 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 2 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 2 |
3 files changed, 3 insertions, 3 deletions
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. |