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/Cyclic/Int31/Cyclic31.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'theories/Numbers/Cyclic/Int31')

diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index f6b2544b6e..c5c75fc17a 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -467,6 +467,7 @@ Section Basics.
  apply phibis_aux_pos.
  Qed.
 
+ #[local]
  Hint Resolve phi_nonneg : zarith.
 
  Lemma phi_bounded  : forall x, (0 <= phi x < 2 ^ (Z.of_nat size))%Z.
-- 
cgit v1.2.3