From 25da65499c986f50d584d7ef38c0762f76df8b31 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 27 Nov 2018 13:25:46 +0100
Subject: Fix #9076 (warning appears when running test suite)

---
 test-suite/modules/Nat.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/modules')

diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
index d2116d2183..95daa1bb0c 100644
--- a/test-suite/modules/Nat.v
+++ b/test-suite/modules/Nat.v
@@ -2,7 +2,7 @@ Definition T := nat.
 
 Definition le := le.
 
-Hint Unfold le.
+Hint Unfold le : core.
 
 Lemma le_refl : forall n : nat, le n n.
   auto.
-- 
cgit v1.2.3