From 4d6892730eece0a99b9c8a86dac6f57bd7939ff4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Mon, 19 Dec 2016 13:34:54 +0100
Subject: [PATCH] make continuation context constructor print properly
---
theories/typing/cont_context.v | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 2f22221b..e065d72c 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -4,7 +4,7 @@ From lrust.lang Require Import notation.
From lrust.lifetime Require Import definitions.
From lrust.typing Require Import type lft_contexts type_context.
-Section cont_context.
+Section cont_context_def.
Context `{typeG Σ}.
Definition cont_postcondition : iProp Σ := False%I.
@@ -13,6 +13,11 @@ Section cont_context.
CctxElt { cctxe_k : val; cctxe_L : llctx;
cctxe_n : nat; cctxe_T : vec val cctxe_n → tctx }.
Definition cctx := list cctx_elt.
+End cont_context_def.
+Add Printing Constructor cctx_elt.
+
+Section cont_context.
+ Context `{typeG Σ}.
Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
let 'CctxElt k L n T := x in
--
GitLab