From 530ce019b7bdcc2603027082f6b3f6841d5990e1 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 16 May 2017 18:28:41 +0200 Subject: Stop using auto with * in two proofs. auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db. --- theories/Structures/DecidableType.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Structures') diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index f85222dfb..d811f04ef 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -86,7 +86,7 @@ Module KeyDecidableType(D:DecidableType). Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. - intros; apply InA_eqA with p; auto with *. + intros; apply InA_eqA with p; auto using eqk_equiv. Qed. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). @@ -109,7 +109,7 @@ Module KeyDecidableType(D:DecidableType). Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. + intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. -- cgit v1.2.3