From 25a16da6a05cd9f3a7dee14157ba8fe086a61a74 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 6 Jan 2017 13:45:55 +0100
Subject: [PATCH] fix build

---
 theories/typing/programs.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 12110588..e5ae5ee4 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -63,7 +63,6 @@ Section typing.
         ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
           (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
             elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
-            elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
   Global Arguments typed_write _%EL _%LL _%T _%T _%T.
 
   (* Technically speaking, we could remvoe the vl quantifiaction here and use
-- 
GitLab