improved auto goal selection (see coq/#16293)

mit-plv · Jul 12, 2022 · 66fd053 · 66fd053
1 parent 2fd296f
commit 66fd053
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Kami/InlineFacts.v b/Kami/InlineFacts.v
@@ -415,7 +415,7 @@ Proof.
   remember (M.find a ds) as odv; destruct odv.
   - remember (M.find a cs) as ocv; destruct ocv; [|apply IHdmsAll].
     destruct (signIsEq s s0); [|destruct (signIsEq _ _); intuition; apply IHdmsAll].
-    subst; destruct (signIsEq s0 s0); intuition auto.
+    subst; destruct (signIsEq s0 s0); intuition idtac.
     rewrite IHdmsAll; simpl in *.
     clear; f_equal.
   - destruct (M.find a cs); apply IHdmsAll.

diff --git a/Kami/SemFacts.v b/Kami/SemFacts.v
@@ -216,8 +216,8 @@ Proof.
     destruct Heqokm as [sm [? ?]]; subst.
     rewrite M.add_idempotent.
     unfold liftToMap1.
-    rewrite M.F.P.fold_add; auto.
-    rewrite M.F.P.fold_add; auto.
+    rewrite M.F.P.fold_add; [|auto|auto| |auto].
+    rewrite M.F.P.fold_add; [|auto|auto| |auto].
     unfold rmModify; simpl in *.
     rewrite M.add_idempotent; reflexivity.
     + apply M.transpose_neqkey_eq_add; intuition.