From 49500e189c9b2aec94922a8661c5215576233ee4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 22 Dec 2016 00:00:43 +0100
Subject: [PATCH] change cont_postcondition to True... because we can, and
 because that would allow us to show adequacy with a terminating continuation

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

diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 9bd73963..b9c109be 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -7,7 +7,7 @@ From lrust.typing Require Import type lft_contexts type_context.
 Section cont_context_def.
   Context `{typeG Σ}.
 
-  Definition cont_postcondition : iProp Σ := False%I.
+  Definition cont_postcondition : iProp Σ := True%I.
 
   Record cctx_elt : Type :=
     CCtx_iscont { cctxe_k : val; cctxe_L : llctx;
-- 
GitLab