diff --git a/barrier/client.v b/barrier/client.v
index 3db716f0f19739d8a6e8942ebf2e48d8cf7a6f0b..5d8132fda4faec90c991d3112e526d111b3138dd 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -7,8 +7,7 @@ Definition client := (let: "b" := newchan '() in wait "b")%L.
 Section client.
   Context {Σ : iFunctorG} (N : namespace).
   Context `{heapG Σ} (heapN : namespace).
-  Context `{stsG heap_lang Σ barrier_proto.sts}.
-  Context `{savedPropG heap_lang Σ}.
+  Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}.
 
   Local Notation iProp := (iPropG heap_lang Σ).