Use `core` database.

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)).

[Ralf Jung]

@robbertkrebbers What does this do and why?

[Robbert]

https://github.com/coq/coq/pull/8987

We have done this at most places already, see 4d6d497a, but somehow we forgot it here.