diff --git a/theories/base_logic/lib/gc.v b/theories/base_logic/lib/gc.v
index 801684ea85a5d01e55a30383b5b5c1c429e36b6c..691aab0df38facc17788c8dbfcb9b2f801b88659 100644
--- a/theories/base_logic/lib/gc.v
+++ b/theories/base_logic/lib/gc.v
@@ -155,7 +155,7 @@ Section gc.
 
   Lemma gc_is_gc l v I : gc_mapsto l v I -∗ is_gc_loc l I.
   Proof.
-    iIntros "Hgc_l". rewrite /gc_mapsto.
+    iIntros "Hgc_l". rewrite /gc_mapsto /is_gc_loc.
     (* We need to help Coq type inference... *)
     change (V → Prop) with (ofe_car $ leibnizO (V → Prop)) in I.
     (* FIXME: is there any good way to avoid repeating the goal here? *)
@@ -224,7 +224,7 @@ Section gc.
       { by apply lookup_to_gc_map_Some in Hsome. }
       apply: prod_local_update_1.  apply: option_local_update.
       apply: exclusive_local_update. done. }
-    iDestruct (big_sepM_insert _ _ _ (w, I) with "[Hl HsepM]") as "HsepM"; [ | by iFrame | ].
+    iDestruct (big_sepM_insert _ _ _ (w, I) with "[$HsepM $Hl //]") as "HsepM".
     { apply lookup_delete. }
     rewrite insert_delete -to_gc_map_insert. iModIntro. iFrame.
     iMod ("Hclose" with "[H● HsepM]"); [ iExists _; by iFrame | by iModIntro].