diff --git a/barrier/client.v b/barrier/client.v index 5d8132fda4faec90c991d3112e526d111b3138dd..7726105ceb2e5a3ba3f5fa1cba76af666389c21e 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 Σ).