aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--test-suite/modules/Nat.v2
1 files changed, 1 insertions, 1 deletions
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.