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/Relations/Relation_Definitions.v | 3 +++
 theories/Relations/Relation_Operators.v   | 3 +++
 2 files changed, 6 insertions(+)

(limited to 'theories/Relations')

diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index 7d0dffdd00..d0d633a0c4 100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -68,10 +68,13 @@ Section Relation_Definition.
 
 End Relation_Definition.
 
+#[global]
 Hint Unfold reflexive transitive antisymmetric symmetric: sets.
 
+#[global]
 Hint Resolve Build_preorder Build_order Build_equivalence Build_PER
   preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl
   equiv_trans equiv_sym per_sym per_trans: sets.
 
+#[global]
 Hint Unfold inclusion same_relation commut: sets.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index f0f36149d1..520333332a 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -228,8 +228,11 @@ Section Lexicographic_Exponentiation.
 
 End Lexicographic_Exponentiation.
 
+#[global]
 Hint Unfold transp union: sets.
+#[global]
 Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets.
+#[global]
 Hint Immediate rst_sym: sets.
 
 (* begin hide *)
-- 
cgit v1.2.3