Adapt w.r.t. coq/coq#18909. (#413)

mit-plv · Apr 9, 2024 · abc59b6 · abc59b6
1 parent 66c47ba
commit abc59b6
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 9 deletions.
diff --git a/bedrock2/src/bedrock2/Map/SeparationLogic.v b/bedrock2/src/bedrock2/Map/SeparationLogic.v
@@ -140,7 +140,7 @@ Section SepProperties.
 
   (* sep and emp *)
   Lemma sep_emp_emp P Q : @iff1 map (sep (emp P) (emp Q)) (emp (P /\ Q)).
-  Proof. cbv [iff1 sep emp split]; t; intuition eauto 20 using putmany_empty_l, disjoint_empty_l. Qed.
+  Proof. cbv [iff1 sep emp split]; t; pose putmany_empty_l; pose disjoint_empty_l; intuition eauto 20. Qed.
   Lemma sep_comm_emp_r p Q : iff1 (p * emp Q) (emp Q * p). eapply sep_comm. Qed.
   Lemma sep_emp_2 p Q r : iff1 (p * (emp Q * r)) (emp Q * (p * r)).
   Proof. rewrite <-sep_assoc. rewrite (sep_comm p). rewrite sep_assoc. reflexivity. Qed.
@@ -173,9 +173,9 @@ Section SepProperties.
 
   (* impl1 and emp *)
   Lemma impl1_l_sep_emp (a:Prop) r c : impl1 (emp a * r) c <-> (a -> impl1 r c).
-  Proof. cbv [impl1 emp sep split]; t; rewrite ?putmany_empty_l; eauto 10 using putmany_empty_l, disjoint_empty_l. Qed.
+  Proof. cbv [impl1 emp sep split]; t; rewrite ?putmany_empty_l; pose putmany_empty_l; pose disjoint_empty_l; eauto 10. Qed.
   Lemma impl1_r_sep_emp p b c : (b /\ impl1 p c) -> impl1 p (emp b * c).
-  Proof. cbv [impl1 emp sep split]; t; eauto 10 using putmany_empty_l, disjoint_empty_l. Qed.
+  Proof. cbv [impl1 emp sep split]; t; pose putmany_empty_l; pose disjoint_empty_l; eauto 10. Qed.
 
 (** shallow reflection from a list of predicates for faster cancellation proofs *)
   Fixpoint seps' (xs : list (map -> Prop)) : map -> Prop :=

diff --git a/compiler/src/compiler/DeadCodeElim.v b/compiler/src/compiler/DeadCodeElim.v
@@ -284,15 +284,15 @@ Section WithArguments1.
       eapply agree_on_union in H2p0; fwd.
       eapply @exec.if_true.
       + erewrite agree_on_eval_bcond; [ eassumption | ].
-        eauto using agree_on_comm. 
+        pose agree_on_comm; eauto.
       + eauto.
     - intros.
       repeat listset_to_set.
       eapply agree_on_union in H2; fwd.
       eapply agree_on_union in H2p0; fwd.
       eapply @exec.if_false.
       + erewrite agree_on_eval_bcond; [ eassumption | ].
-        eauto using agree_on_comm. 
+        pose agree_on_comm; eauto.
       + eauto.
     - intros.
       cbn - [live].

diff --git a/compiler/src/compiler/FlattenExpr.v b/compiler/src/compiler/FlattenExpr.v
@@ -677,7 +677,7 @@ Section FlattenExpr1.
     + left. clear P.
       intro. apply Ino.
       epose proof (ExprImp.allVars_cmd_allVars_cmd_as_list _ _) as P. destruct P as [P _].
-      eauto using ListSet.In_list_union_l, ListSet.In_list_union_r, nth_error_In.
+      pose ListSet.In_list_union_l; pose ListSet.In_list_union_r; pose nth_error_In; eauto.
   Qed.
 
   Lemma flattenStmt_correct_aux: forall eH eL,
@@ -888,7 +888,7 @@ Section FlattenExpr1.
              unfold map.of_list_zip in G.
              eapply map.putmany_of_list_zip_find_index in G. 2: eassumption.
              rewrite map.get_empty in G. destruct G as [G | G]; [|discriminate G]. simp.
-             eauto using ListSet.In_list_union_l, ListSet.In_list_union_r, nth_error_In.
+             pose ListSet.In_list_union_l; pose ListSet.In_list_union_r; pose nth_error_In; eauto.
           -- eapply freshNameGenState_disjoint_fbody.
         * cbv beta. intros. simp.
           edestruct H4 as [resvals ?]. 1: eassumption. simp.

diff --git a/compiler/src/compiler/SeparationLogic.v b/compiler/src/compiler/SeparationLogic.v
@@ -503,15 +503,15 @@ Section MoreSepLog.
     intros. eapply iff1ToEq.
     unfold iff1, sep, map.split. split; intros.
     - destruct H as (? & ? & (? & ?) & ? & ?). subst. rewrite map.putmany_empty_l. assumption.
-    - eauto 10 using map.putmany_empty_l, map.disjoint_empty_l.
+    - pose map.putmany_empty_l; pose map.disjoint_empty_l; eauto 10.
   Qed.
 
   Lemma sep_eq_empty_r: forall (R: map -> Prop), (R * eq map.empty)%sep = R.
   Proof.
     intros. eapply iff1ToEq.
     unfold iff1, sep, map.split. split; intros.
     - destruct H as (? & ? & (? & ?) & ? & ?). subst. rewrite map.putmany_empty_r. assumption.
-    - eauto 10 using map.putmany_empty_r, map.disjoint_empty_r.
+    - pose map.putmany_empty_r; pose map.disjoint_empty_r; eauto 10.
   Qed.
 
   Lemma get_in_sep: forall (lSmaller l: map) k v R,