From 68cd077344ce37db1a601079dbc4fdcae6c8d41f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 14 Nov 2020 17:55:07 +0100
Subject: Explicitly annotate all hint declarations of the standard library.

By default Coq stdlib warnings raise an error, so this is really required.
---
 theories/Numbers/Natural/Abstract/NDefOps.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'theories/Numbers/Natural/Abstract/NDefOps.v')

diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 019b138b4d..2f8fcc7290 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -383,6 +383,7 @@ f_equiv. apply E, half_decrease.
 rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
 order'.
 Qed.
+#[global]
 Hint Resolve log_good_step : core.
 
 Theorem log_init : forall n, n < 2 -> log n == 0.
-- 
cgit v1.2.3