diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v index 4a48c547a57cbd3e0bc28c034ea103fcd72116ab..eb21d09df4c92421d173a1cfb2ed34f4b90baeee 100644 --- a/theories/typing/lib/rc/rc.v +++ b/theories/typing/lib/rc/rc.v @@ -356,7 +356,7 @@ Section code. wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz. wp_apply (wp_memcpy with "[$Hrcbox↦2 $Hx↦]"); [by auto using vec_to_list_length..|]. - iIntros "[Hrcbox↦2 Hx↦]". wp_seq. wp_op. rewrite shift_loc_0. wp_write. + iIntros "[Hrcbox↦2 Hx↦]". wp_seq. wp_write. iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (rc ty)] with "[] LFT HE Hna HL Hk [-]"); last first. { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame. @@ -760,6 +760,5 @@ Section code. (* TODO: * fn make_mut(this: &mut Rc<T>) -> &mut T Needs a Clone bound, how do we model this? - * Weak references? *) End code.