From df18abd2623d35a70e32d4c722c1d45e74e567db Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 19 Jan 2017 09:26:02 +0100
Subject: [PATCH] fix typo in unmk_cell

---
 theories/typing/unsafe/cell.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index f752401f..2020e193 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -67,7 +67,7 @@ Section typing.
 
   (* Same for the other direction *)
   Lemma tctx_unmk_cell E L ty p :
-    tctx_incl E L [p ◁ ty] [p ◁ cell ty].
+    tctx_incl E L [p ◁ cell ty] [p ◁ ty].
   Proof.
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
-- 
GitLab