diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 7f3fa099052046c9bab4d45997701c507872b51b..c2cfca78955f5c319c53868f381fbb68730bd47e 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -8,10 +8,10 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Class typePreG Σ := PreTypeG {
-  type_heapG :> lrustPreG Σ;
-  type_lftG :> lftPreG Σ;
+  type_preG_lrustG :> lrustPreG Σ;
+  type_preG_lftG :> lftPreG Σ;
   type_preG_na_invG :> na_invG Σ;
-  type_frac_borrowG :> frac_borG Σ
+  type_preG_frac_borG :> frac_borG Σ
 }.
 
 Definition typeΣ : gFunctors :=
diff --git a/theories/typing/type.v b/theories/typing/type.v
index a943dab5b699bd0beb20f2af6f3a535370531e12..2cecc1eb20f6d0c3685e85722033d822dd1e3649 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -7,7 +7,7 @@ From lrust.typing Require Import lft_contexts.
 Set Default Proof Using "Type".
 
 Class typeG Σ := TypeG {
-  type_heapG :> lrustG Σ;
+  type_lrustG :> lrustG Σ;
   type_lftG :> lftG Σ;
   type_na_invG :> na_invG Σ;
   type_frac_borrowG :> frac_borG Σ