adapt for coq/coq#17022

mit-plv · Feb 14, 2023 · 7e6d138 · 7e6d138
1 parent 2a4260d
commit 7e6d138
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/Kami/InlineFacts.v b/Kami/InlineFacts.v
@@ -7,6 +7,8 @@ Require Import Kami.RefinementFacts.
 
 Require Import FunctionalExtensionality.
 
+Require Btauto.
+
 Set Implicit Arguments.
 Set Asymmetric Patterns.
 
@@ -1327,8 +1329,7 @@ Proof.
     + auto.
   - apply andb_true_iff in H; dest.
     apply andb_true_iff in H; dest.
-    apply andb_true_iff; split; auto.
-    apply andb_true_iff; split; auto.
+    auto 9 using andb_true_iff.
 Qed.
 
 Lemma noCalls_noCallDmSigATrue:
@@ -1362,7 +1363,7 @@ Lemma inlineDm_noCallDmSigA:
     noCallDmSigA (inlineDm a dm) (attrName dm) (projT1 (attrType dm)) = true.
 Proof.
   induction a; simpl; intros; auto;
-    [|do 2 (apply andb_true_iff; split; auto)].
+    (try solve [do 2 (apply andb_true_iff; split; auto)]); [ ].
 
   unfold getBody.
   remember (string_eq meth (attrName dm)) as md; destruct md;