From 66fd05345a4993f5eb5a36d5756cf43ea1bfa074 Mon Sep 17 00:00:00 2001 From: Andrej Dudenhefner Date: Tue, 12 Jul 2022 09:19:08 +0200 Subject: [PATCH] improved auto goal selection (see coq/#16293) --- Kami/InlineFacts.v | 2 +- Kami/SemFacts.v | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Kami/InlineFacts.v b/Kami/InlineFacts.v index fc83ebef..bb1c6300 100644 --- 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 index d8a69c1a..43c469d5 100644 --- 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.