From 6f737edae4b7e6243a9f11e74614f55381f62ec7 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 2 Aug 2019 10:41:29 +0200
Subject: Coq 8.10 compatibility: make explicit the "core" hint database

"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".
---
 backend/Conventions.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'backend/Conventions.v')

diff --git a/backend/Conventions.v b/backend/Conventions.v
index 989bfa05..6025c6b4 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -128,8 +128,6 @@ Definition callee_save_loc (l: loc) :=
   | S sl ofs ty => sl <> Outgoing
   end.
 
-Hint Unfold callee_save_loc.
-
 Definition agree_callee_save (ls1 ls2: Locmap.t) : Prop :=
   forall l, callee_save_loc l -> ls1 l = ls2 l.
 
-- 
cgit