diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index ee19d85814f75fa4d2a3e55400c8ea295424435d..5a065a01fcf26eea56a1fc8f3fd556a68f897afb 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -38,7 +38,8 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
   (l ↦ NONEV ∗ own γ (Pending (1/2)%Qp) ∨
    ∃ n : Z, l ↦ SOMEV #n ∗ own γ (Shot n))%I.
 
-Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) => unfold one_shot_inv.
+Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) =>
+  unfold one_shot_inv : core.
 
 Lemma pending_split γ q :
   own γ (Pending q) ⊣⊢ own γ (Pending (q/2)) ∗ own γ (Pending (q/2)).