Commit 32daff99 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove obsolute FIXME.

parent 45f84a82
Pipeline #78 passed with stage
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.
......
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