From a1b6f914b12d3f7c35741acc2f6c83f1a47813ba Mon Sep 17 00:00:00 2001 From: Andrej Dudenhefner Date: Mon, 11 Jul 2022 14:57:11 +0200 Subject: [PATCH] improved auto goal selection (see coq/#16293) --- theories/Data/Map/FMapAList.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Data/Map/FMapAList.v b/theories/Data/Map/FMapAList.v index 72b2f15..47c0bc4 100644 --- a/theories/Data/Map/FMapAList.v +++ b/theories/Data/Map/FMapAList.v @@ -53,7 +53,7 @@ Section keyed. induction m; intuition. unfold alist_find', compose. simpl. - destruct (k ?[ R ] a0) eqn:Heq; intuition. + destruct (k ?[ R ] a0) eqn:Heq; [intuition|]. rewrite IHm. reflexivity. Qed.