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/FSets/FSetDecide.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'theories/FSets/FSetDecide.v')

diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 8a217a752a..d597c0404a 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -466,6 +466,7 @@ the above form:
     (** Here is the tactic that will throw away hypotheses that
         are not useful (for the intended scope of the [fsetdec]
         tactic). *)
+    #[global]
     Hint Constructors FSet_elt_Prop FSet_Prop : FSet_Prop.
     Ltac discard_nonFSet :=
       repeat (
@@ -518,6 +519,7 @@ the above form:
 
     (** The hint database [FSet_decidability] will be given to
         the [push_neg] tactic from the module [Negation]. *)
+    #[global]
     Hint Resolve dec_In dec_eq : FSet_decidability.
 
     (** ** Normalizing Propositions About Equality
-- 
cgit v1.2.3