diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v index 3a517ebaed542dc511e1f407697948693435e349..08e45f56905b346bb1e3bb91a5f0a977f8b78e75 100644 --- a/heap_lang/lib/barrier/specification.v +++ b/heap_lang/lib/barrier/specification.v @@ -9,7 +9,6 @@ Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}. Local Notation iProp := (iPropG heap_lang Σ). -(* TODO: Maybe notation for LocV (and Loc)? *) Lemma barrier_spec (heapN N : namespace) : heapN ⊥ N → ∃ recv send : loc → iProp -n> iProp,