diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v index ec3b3ad28d84a7b5621e6b3f7ec7c653ef665c87..41f23cb4e9e077c417ef1ea8ab0453fe98c19eeb 100644 --- a/iris/base_logic/lib/gen_heap.v +++ b/iris/base_logic/lib/gen_heap.v @@ -237,7 +237,7 @@ Section gen_heap. rewrite meta_unseal /meta_def. iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)". iCombine "Hγm1 Hγm2" gives %[_ ->]. - iCombine "Hm1 Hm2" gives %Hγ. iPureIntro. + iCombine "Hm1 Hm2" gives %Hγ; iPureIntro. move: Hγ. rewrite -reservation_map_data_op reservation_map_data_valid. move=> /to_agree_op_inv_L. naive_solver. Qed. diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v index 30a59b09a303480da411dcc31808d8f2c3834e4a..9361c44182e1f0d15e8abeb48b9c9a35e4a9468f 100644 --- a/iris/base_logic/lib/ghost_var.v +++ b/iris/base_logic/lib/ghost_var.v @@ -63,7 +63,7 @@ Section lemmas. ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜a1 = a2âŒ. Proof. iIntros "Hvar1 Hvar2". - iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ->]. done. + iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done. Qed. Global Instance ghost_var_combine_gives γ a1 q1 a2 q2 : diff --git a/iris/bi/lib/cmra.v b/iris/bi/lib/cmra.v index 65fca318a02bc042656e7618ea54ab226a2102dd..f3a8b9a20f46e2d9f19823c2242b48da1a74daed 100644 --- a/iris/bi/lib/cmra.v +++ b/iris/bi/lib/cmra.v @@ -149,4 +149,4 @@ Section internal_included_laws. + iIntros "[%z Hz]". iRewrite "Hz". by rewrite assoc agree_idemp. + iIntros "H". by iExists _. Qed. -End internal_included_laws. +End internal_included_laws. \ No newline at end of file