diff --git a/barrier/barrier.v b/barrier/barrier.v
index 0dbf4b8f1662318484766b5445402e272488d8f7..97efedbb5ddd488123dc7f6b9e29f73cf7972ef7 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -125,7 +125,7 @@ End barrier_proto.
 Import barrier_proto.
 
 (* The functors we need. *)
-Definition barrierFs := stsF sts `::` agreeF `::` pnil.
+Definition barrierGFs := stsGF sts `::` agreeF `::` pnil.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
diff --git a/barrier/client.v b/barrier/client.v
index 29bd737be4e649c7b950a8bc436312b9f92b56bb..47bf44ebda396288d69e3051036e134bd0cddab9 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -26,7 +26,7 @@ Section client.
 End client.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := heapF .:: barrierFs .++ endF.
+  Definition Σ : iFunctorG := heapGF .:: barrierGFs .++ endGF.
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 2a32e5ffc3955604a0bdfac6bad94d445e1905b1..7e517f24b4338a7d189f9e9fad60682378c0fa5e 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -7,8 +7,8 @@ Import uPred.
    a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
    predicates over finmaps instead of just ownP. *)
 
-Definition heapRA := mapRA loc (exclRA (leibnizC val)).
-Definition heapF := authF heapRA.
+Definition heapRA : cmraT := mapRA loc (exclRA (leibnizC val)).
+Definition heapGF : iFunctor := authGF heapRA.
 
 Class heapG Σ := HeapG {
   heap_inG : inG heap_lang Σ (authRA heapRA);
@@ -21,7 +21,7 @@ Definition to_heap : state → heapRA := fmap Excl.
 Definition of_heap : heapRA → state := omap (maybe Excl).
 
 Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
-  auth_own heap_name ({[ l := Excl v ]} : heapRA).
+  auth_own heap_name {[ l := Excl v ]}.
 Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
   ownP (of_heap h).
 Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
@@ -104,7 +104,7 @@ Section heap.
     P ⊑ || Alloc e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
-    trans (|={E}=> auth_own heap_name (∅ : heapRA) ★ P)%I.
+    trans (|={E}=> auth_own heap_name ∅ ★ P)%I.
     { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
     apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 0f8467db59e8cfe3d0557f216c38972d00765068..71a7f35afcf8a355dc348151fb6b1fc7953a87d8 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -76,7 +76,7 @@ Section LiftingTests.
 End LiftingTests.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := heapF .:: endF.
+  Definition Σ : iFunctorG := heapGF .:: endGF.
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 2e7f75d709503b3c03b5159092918eae8366eb89..d056d51cc600daa1a2672b2a6ee06a74394ff96f 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -9,12 +9,10 @@ Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_timeless (a : A) :> Timeless a;
 }.
 
-(* TODO: This shadows algebra.auth.authF. *)
-Definition authF (A : cmraT) := constF (authRA A).
-
-Instance authG_inGF (A : cmraT) `{CMRAIdentity A} `{∀ a : A, Timeless a}
-         `{inGF Λ Σ (authF A)} : authG Λ Σ A.
-Proof. split; try apply _. move:(@inGF_inG Λ Σ (authF A)). auto. Qed.
+Definition authGF (A : cmraT) : iFunctor := constF (authRA A).
+Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
+  `{CMRAIdentity A, ∀ a : A, Timeless a} : authG Λ Σ A.
+Proof. split; try apply _. apply: inGF_inG. Qed.
 
 Section definitions.
   Context `{authG Λ Σ A} (γ : gname).
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index b42995bf062c3e70b787849de396fce0e74b8c62..d66734f70e0e86ff4256e3d21b38b8221d6591d8 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -28,6 +28,30 @@ Typeclasses Opaque to_globalF own.
 Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
 Notation iFunctorG := (gid → iFunctor).
 
+(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
+   the functor breaks badly because Coq is unable to infer the correct
+   typeclasses, it does not unfold the functor. *)
+Class inGF (Λ : language) (Σ : gid → iFunctor) (F : iFunctor) := InGF {
+  inGF_id : gid;
+  inGF_prf : F = Σ inGF_id;
+}.
+(* Avoid eager type class search: this line ensures that type class search
+is only triggered if the first two arguments of inGF do not contain evars. Since
+instance search for [inGF] is restrained, instances should always have [inGF] as
+their first argument to avoid loops. For example, the instances [authGF_inGF]
+and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
+Hint Mode inGF + + - : typeclass_instances.
+
+Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
+Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
+Instance inGF_here {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
+Proof. by exists 0. Qed.
+Instance inGF_further {Λ Σ} (F F': iFunctor) : inGF Λ Σ F → inGF Λ (F' .:: Σ) F.
+Proof. intros [i ?]. by exists (S i). Qed.
+
+Definition endGF : iFunctorG := const (constF unitRA).
+
+(** Properties about ghost ownership *)
 Section global.
 Context `{i : inG Λ Σ A}.
 Implicit Types a : A.
@@ -145,22 +169,3 @@ Proof.
   apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
 Qed.
 End global.
-
-(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
-   the functor breaks badly because Coq is unable to infer the correct
-   typeclasses, it does not unfold the functor. *)
-Class inGF (Λ : language) (Σ : gid → iFunctor) (F : iFunctor) := InGF {
-  inGF_id : gid;
-  inGF_prf : F = Σ inGF_id;
-}.
-
-Instance inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
-Proof. exists inGF_id. f_equal. apply inGF_prf. Qed.
-
-Instance inGF_nil {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
-Proof. exists 0. done. Qed.
-
-Instance inGF_cons `{inGF Λ Σ F} (F': iFunctor) : inGF Λ (F' .:: Σ) F.
-Proof. exists (S inGF_id). apply inGF_prf. Qed.
-
-Definition endF : gid → iFunctor := const (constF unitRA).
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 6ab24d6127978ea43810ae94326e220b6a03ee8d..1d17c0906f29b0cbe30b75f5970e71d8acdec912 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -6,7 +6,7 @@ Notation savedPropG Λ Σ :=
   (inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
 
 Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
-Proof. move:(@inGF_inG Λ Σ agreeF). auto. Qed.
+Proof. apply: inGF_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
@@ -18,11 +18,9 @@ Section saved_prop.
   Implicit Types P Q : iPropG Λ Σ.
   Implicit Types γ : gname.
 
-  Global Instance : ∀ P, AlwaysStable (saved_prop_own γ P).
-  Proof.
-    intros. rewrite /AlwaysStable /saved_prop_own.
-    rewrite always_own; done.
-  Qed.
+  Global Instance saved_prop_always_stable γ P :
+    AlwaysStable (saved_prop_own γ P).
+  Proof. by rewrite /AlwaysStable /saved_prop_own always_own. Qed.
 
   Lemma saved_prop_alloc_strong N P (G : gset gname) :
     True ⊑ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ P).
diff --git a/program_logic/sts.v b/program_logic/sts.v
index b53c7dcb27ad605e74a8f18b86272fed55ac2fd4..e118a20b145d6365c5247ceae3c85f85debace46 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -8,11 +8,10 @@ Class stsG Λ Σ (sts : stsT) := StsG {
 }.
 Coercion sts_inG : stsG >-> inG.
 
-Definition stsF (sts : stsT) := constF (stsRA sts).
-
-Instance stsG_inGF sts `{Inhabited (sts.state sts)}
-         `{inGF Λ Σ (stsF sts)} : stsG Λ Σ sts.
-Proof. split; try apply _. move:(@inGF_inG Λ Σ (stsF sts)). auto. Qed.
+Definition stsGF (sts : stsT) : iFunctor := constF (stsRA sts).
+Instance stsGF_inGF sts `{inGF Λ Σ (stsGF sts)}
+  `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
+Proof. split; try apply _. apply: inGF_inG. Qed.
 
 Section definitions.
   Context `{i : stsG Λ Σ sts} (γ : gname).