diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-05-16 18:28:41 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-05-16 18:28:41 +0200 |
| commit | 530ce019b7bdcc2603027082f6b3f6841d5990e1 (patch) | |
| tree | cabc0bd3f442df9a7229bff8dd9edd964d342a0f /theories/Structures | |
| parent | 9f8220164703aee47c6c6d7dba07caabf7555c1c (diff) | |
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.
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/DecidableType.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |