Commit 1747d779 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove old todo.

parent 4e2dfc4e
...@@ -9,7 +9,6 @@ Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}. ...@@ -9,7 +9,6 @@ Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}.
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
(* TODO: Maybe notation for LocV (and Loc)? *)
Lemma barrier_spec (heapN N : namespace) : Lemma barrier_spec (heapN N : namespace) :
heapN N heapN N
recv send : loc iProp -n> iProp, recv send : loc iProp -n> iProp,
......
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