diff --git a/barrier/barrier.v b/barrier/barrier.v
index e08d4bbede9195e2aeca3e3b91a5aca8b48f1eb7..c36779a2299af18fb3ad95557272acc9250ad864 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -125,14 +125,14 @@ End barrier_proto.
 Import barrier_proto.
 
 (* The functors we need. *)
-Definition barrierGFs : iFunctors := [stsGF sts; agreeF].
+Definition barrierGF : iFunctors := [stsGF sts; agreeF].
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
   Context {Σ : iFunctorG} (N : namespace).
   Context `{heapG Σ} (heapN : namespace).
-  Context `{stsG heap_lang Σ sts}.
-  Context `{savedPropG heap_lang Σ}.
+  (* These are exactly the elements of barrierGF *)
+  Context `{inGF heap_lang Σ (stsGF sts)} `{inGF heap_lang Σ agreeF}.
 
   Local Hint Immediate i_states_closed low_states_closed : sts.
   Local Hint Resolve signal_step wait_step split_step : sts.
diff --git a/barrier/client.v b/barrier/client.v
index 5db27c1786908ad504e85ce821a315702cb76dbb..3db716f0f19739d8a6e8942ebf2e48d8cf7a6f0b 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -26,7 +26,7 @@ Section client.
 End client.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := #[ heapGF ; barrierGFs ].
+  Definition Σ : iFunctorG := #[ heapGF ; barrierGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index fa01192112ecb1d5f52e882b2334d20b73e7fb80..ee573c93419d30ea568afd4e402f4252a0693176 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -5,7 +5,7 @@ Import uPred.
 Notation savedPropG Λ Σ :=
   (inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
 
-Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
+Instance inGF_savedPropG `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
 Proof. apply: inGF_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Λ Σ}
diff --git a/program_logic/sts.v b/program_logic/sts.v
index a2716da5cff0b57ab0965bf4d40c0b97f9431a2c..b66a60e134db9db0500878dd8f36eabbb8e0c62b 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -9,7 +9,7 @@ Class stsG Λ Σ (sts : stsT) := StsG {
 Coercion sts_inG : stsG >-> inG.
 
 Definition stsGF (sts : stsT) : iFunctor := constF (stsRA sts).
-Instance stsGF_inGF sts `{inGF Λ Σ (stsGF sts)}
+Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
   `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
 Proof. split; try apply _. apply: inGF_inG. Qed.