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/FSets/FMapAVL.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/FSets/FMapAVL.v') 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. -- cgit v1.2.3