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/FSets/FMapAVL.v | |
| parent | a1315d78a5b3c6095848298f03ca328380a7d453 (diff) | |
[stdlib] Remove a few `auto with *`
Diffstat (limited to 'theories/FSets/FMapAVL.v')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 8cdc6e54c5..82055c4752 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1335,7 +1335,7 @@ Proof. apply Hl; auto. constructor. apply Hr; eauto. - apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6. + apply InA_InfA with (eqA:=eqke). auto with typeclass_instances. intros (y',e') H6. destruct (elements_aux_mapsto r acc y' e'); intuition. red; simpl; eauto. red; simpl; eauto with ordered_type. |