From 11231ef7f9946ee21a99b48efe312e5cd00dd3d1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 Jul 2017 14:23:02 -0700
Subject: [PATCH] unfix a FIXME
---
theories/typing/lib/join.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index cc269473..beb8ebef 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -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..|].
--
GitLab