diff --git a/barrier/barrier.v b/barrier/barrier.v
index e473a9cc6f570ee32fa5037b3c88b4cf1282aa79..d610b5ba38a4ea481ba1efb0c57510ad09aa2aab 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -124,15 +124,23 @@ End barrier_proto.
    the module into our namespaces. But Coq doesn't seem to support that...?? *)
 Import barrier_proto.
 
-(* The functors we need. *)
+(** The monoids we need. *)
+(* Not bundling heapG, as it may be shared with other users. *)
+Class barrierG Σ `{heapG Σ} := BarrierG {
+  barrier_stsG :> stsG heap_lang Σ sts;
+  barrier_savedPropG :> savedPropG heap_lang Σ;
+}.
+
 Definition barrierGF : iFunctors := [stsGF sts; agreeF].
 
+Instance inGF_barrierG `{heapG Σ} `{inGF heap_lang Σ (stsGF sts)}
+         `{inGF heap_lang Σ agreeF} : barrierG Σ.
+Proof. split; apply _. Qed.
+
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-  Context {Σ : iFunctorG} (N : namespace).
-  Context `{heapG Σ} (heapN : namespace).
-  (* These are exactly the elements of barrierGF *)
-  Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}.
+  Context {Σ : iFunctorG} `{barrierG Σ}.
+  Context (N : namespace) (heapN : namespace).
 
   Local Hint Immediate i_states_closed low_states_closed : sts.
   Local Hint Resolve signal_step wait_step split_step : sts.
@@ -477,9 +485,7 @@ Section proof.
 End proof.
 
 Section spec.
-  Context {Σ : iFunctorG}.
-  Context `{heapG Σ}.
-  Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}.
+  Context {Σ : iFunctorG} `{!heapG Σ} `{!barrierG Σ}. 
 
   Local Notation iProp := (iPropG heap_lang Σ).
 
diff --git a/barrier/client.v b/barrier/client.v
index 7726105ceb2e5a3ba3f5fa1cba76af666389c21e..c1e88af819247e6b736f89ed917f99b085700641 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -5,10 +5,8 @@ Import uPred.
 Definition client := (let: "b" := newchan '() in wait "b")%L.
 
 Section client.
-  Context {Σ : iFunctorG} (N : namespace).
-  Context `{heapG Σ} (heapN : namespace).
-  (* TODO: This should be abstracted away somehow. *)
-  Context `{inGF heap_lang Σ (stsGF barrier_proto.sts)} `{inGF heap_lang Σ agreeF}.
+  Context {Σ : iFunctorG} `{!heapG Σ} `{!barrierG Σ}.
+  Context (N : namespace) (heapN : namespace).
 
   Local Notation iProp := (iPropG heap_lang Σ).