From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 21 Jan 2021 15:44:09 +0100
Subject: Qualify `Hint` as `Global Hint` where appropriate

This avoids a new warning of Coq 8.13.

Eventually these `Global Hint` should become `#[export] Hint`,
with a cleaner but different meaning than `Global Hint`.
---
 common/Memory.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'common/Memory.v')

diff --git a/common/Memory.v b/common/Memory.v
index 641a9243..b16a98b6 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -4500,7 +4500,7 @@ Notation mem := Mem.mem.
 
 Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes.
 
-Hint Resolve
+Global Hint Resolve
   Mem.valid_not_valid_diff
   Mem.perm_implies
   Mem.perm_cur
-- 
cgit