From 1bb62ee372d66996573c9aa51fe3c4d23488115e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Nov 2019 16:28:19 +0100
Subject: [PATCH] Use `core` database.

---
 tests/one_shot_once.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index ee19d8581..5a065a01f 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)).
-- 
GitLab