Skip to content
Snippets Groups Projects
Commit 11231ef7 authored by Ralf Jung's avatar Ralf Jung
Browse files

unfix a FIXME

parent f8fc6b41
No related branches found
No related tags found
No related merge requests found
......@@ -81,6 +81,7 @@ Section join.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
iApply (type_new_subtype (Π[uninit R_A.(ty_size); uninit R_B.(ty_size)]));
(* FIXME: solve_typing should handle this without any aid. *)
rewrite ?Z_nat_add; [solve_typing..|].
iIntros (r); simpl_subst.
iApply (type_memcpy R_A); [solve_typing..|].
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment