aboutsummaryrefslogtreecommitdiff
path: root/test-suite/modules
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/modules')
-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.