diff --git a/barrier/barrier.v b/barrier/barrier.v
index c36779a2299af18fb3ad95557272acc9250ad864..a08052869afcd12e06bed88332df5b509a196dc6 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -482,8 +482,7 @@ End proof.
 Section spec.
   Context {Σ : iFunctorG}.
   Context `{heapG Σ}.
-  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 Σ).