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

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

diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index ab87ba9722..77ce76721e 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -58,6 +58,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
 Module Type WSfun (E : DecidableType).
 
   Definition key := E.t.
+  #[global]
   Hint Transparent key : core.
 
   Parameter t : Type -> Type.
@@ -243,9 +244,11 @@ Module Type WSfun (E : DecidableType).
 	(x:key)(f:option elt->option elt'->option elt''),
         In x (map2 f m m') -> In x m \/ In x m'.
 
+  #[global]
   Hint Immediate MapsTo_1 mem_2 is_empty_2
     map_2 mapi_2 add_3 remove_3 find_2
     : map.
+  #[global]
   Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
     remove_2 find_1 fold_1 map_1 mapi_1 mapi_2
     : map.
-- 
cgit v1.2.3