improved auto goal selection (see coq/#16293)

coq-community · Jul 12, 2022 · a1b6f91 · a1b6f91
1 parent bf494bf
commit a1b6f91
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.