From 0657f6bfa8d9ae00215cc720799314d0a3921273 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 9 Dec 2016 19:02:31 +0100
Subject: [PATCH] Stuck.
---
theories/typing/perm.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index e7f15200..b543b951 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -118,7 +118,7 @@ Section has_type.
WP ν @ E {{ Φ }}.
Proof.
iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type.
- destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]".
+ destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". simpl.
iMod ("HΦ" $! v with "[] H◁") as "HΦ". done.
iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
forall (Φ v EQν); try done.
--
GitLab