diff --git a/barrier/client.v b/barrier/client.v index 5e888030cf26009598b28cc906f00cfded651bca..29bd737be4e649c7b950a8bc436312b9f92b56bb 100644 --- a/barrier/client.v +++ b/barrier/client.v @@ -1,7 +1,5 @@ From barrier Require Import barrier. From program_logic Require Import auth sts saved_prop hoare ownership. -(* FIXME This needs to be imported even though barrier exports it *) -From heap_lang Require Import notation. Import uPred. Definition client := (let: "b" := newchan '() in wait "b")%L.