diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index c147dede368126ff229137b1504fa312dc1a23a8..ba10b34fc37f188c343c636203533bf51e22485f 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -66,7 +66,7 @@ Section definitions.
          ∗ ⌜heap_freeable_rel σ hF⌝)%I.
 End definitions.
 
-Global Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
+Global Typeclasses Opaque heap_mapsto_vec.
 Global Instance: Params (@heap_mapsto) 4 := {}.
 Global Instance: Params (@heap_freeable) 5 := {}.
 
@@ -127,8 +127,7 @@ Section heap.
   Global Instance frame_mapsto p l v q1 q2 q :
     FrameFractionalQp q1 q2 q →
     Frame p (l ↦{q1} v) (l ↦{q2} v) (l ↦{q} v) | 5.
-  (* FIXME: somehow Φ gets inferred wrong here. *)
-  Proof. apply: (frame_fractional _ _ _ (λ q, l ↦{q} v)%I). Qed.
+  Proof. apply: frame_fractional. Qed.
 
   Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
   Proof. rewrite /heap_mapsto_vec. apply _. Qed.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index edbf417439c7e4b4eae624f524d9b967577a86ee..cf2e327f63426606e8d77aa38d2422a71fdbb8a9 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -322,8 +322,8 @@ Global Instance lft_tok_as_fractional κ q :
   AsFractional q.[κ] (λ q, q.[κ])%I q.
 Proof. split; first done. apply _. Qed.
 Global Instance frame_lft_tok p κ q1 q2 q :
-    FrameFractionalQp q1 q2 q →
-    Frame p q1.[κ] q2.[κ] q.[κ] | 5.
+  FrameFractionalQp q1 q2 q →
+  Frame p q1.[κ] q2.[κ] q.[κ] | 5.
 (* FIXME: somehow Φ gets inferred wrong here. *)
 Proof. apply: (frame_fractional _ _ _ (λ q, q.[κ])%I). Qed.
 
@@ -336,8 +336,8 @@ Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
 Proof. split; first done. apply _. Qed.
 Global Instance frame_idx_bor_own p i q1 q2 q :
-    FrameFractionalQp q1 q2 q →
-    Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
+  FrameFractionalQp q1 q2 q →
+  Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
 (* FIXME: somehow Φ gets inferred wrong here. *)
 Proof. apply: (frame_fractional _ _ _ (λ q, idx_bor_own q i)%I). Qed.