Commit 7e6fe5f0 authored by Ralf Jung's avatar Ralf Jung

today is not my day...

parent 448f2f1e
Pipeline #90 passed with stage
......@@ -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 Σ).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment