From 7e6fe5f004fe839d22dd317d2c6c3c86c9cc0109 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 23 Feb 2016 11:31:38 +0100 Subject: [PATCH] today is not my day... --- barrier/client.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/barrier/client.v b/barrier/client.v index 5d8132fda..7726105ce 100644 --- a/barrier/client.v +++ b/barrier/client.v @@ -7,7 +7,8 @@ Definition client := (let: "b" := newchan '() in wait "b")%L. Section client. Context {Σ : iFunctorG} (N : namespace). Context `{heapG Σ} (heapN : namespace). - Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}. + (* TODO: This should be abstracted away somehow. *) + Context `{inGF heap_lang Σ (stsGF barrier_proto.sts)} `{inGF heap_lang Σ agreeF}. Local Notation iProp := (iPropG heap_lang Σ). -- GitLab