From 1df2fadbf5ab0687d2aac52f3a83bbe071c25139 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 9 Mar 2020 08:07:04 +0100
Subject: removing some coqc 8.10 warnings

---
 backend/Duplicateproof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend/Duplicateproof.v')

diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index a8e9b16b..466b4b75 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -378,7 +378,7 @@ Theorem step_simulation:
      step tge s2 t s2'
   /\ match_states s1' s2'.
 Proof.
-  Local Hint Resolve transf_fundef_correct.
+  Local Hint Resolve transf_fundef_correct: core.
   induction 1; intros; inv MS.
 (* Inop *)
   - eapply dupmap_correct in DUPLIC; eauto.
-- 
cgit