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/FSetBridge.v | 3 +++
 1 file changed, 3 insertions(+)

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

diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 73021a84a3..4917fcb5fd 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -137,6 +137,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
     generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder.
   Qed.
 
+  #[global]
   Hint Resolve compat_P_aux : core.
 
   Definition filter :
@@ -467,6 +468,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
   Proof.
     intros; unfold elements; case (M.elements s); firstorder.
   Qed.
+  #[global]
   Hint Resolve elements_3 : core.
 
   Lemma elements_3w : forall s : t, NoDupA E.eq (elements s).
@@ -666,6 +668,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
       rewrite <- H1; firstorder.
   Qed.
 
+  #[global]
   Hint Resolve compat_P_aux : core.
 
   Definition filter (f : elt -> bool) (s : t) : t :=
-- 
cgit v1.2.3