Skip to content
Snippets Groups Projects

Enable mangled names

Merged Enable mangled names
ci/weak_mem_mangle_names into masters/weak_mem
Merged Hai Dang requested to merge ci/weak_mem_mangle_names into masters/weak_mem
Compare
and
2 files
+ 1
− 1
Compare changes
  • Side-by-side
  • Inline
Files
2
theories/lang/memcpy.v
+ 0
− 1
@@ -32,7 +32,6 @@ Proof.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !own_loc_na_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
Qed.