Explicitly annotate all hint declarations of the standard library.

By default Coq stdlib warnings raise an error, so this is really required.

4 files changed, 6 insertions, 0 deletions

diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v
index 31d9f7f0ed..cebb0c808c 100644
--- a/theories/Sorting/CPermutation.v
+++ b/theories/Sorting/CPermutation.v
@@ -96,6 +96,7 @@ Qed.
 
 End CPermutation.
 
+#[global]
 Hint Resolve CPermutation_refl : core.
 
 (* These hints do not reduce the size of the problem to solve and they
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 1130c9dd76..05a21620b7 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -36,7 +36,9 @@ Section defs.
   Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
   Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
 
+  #[local]
   Hint Resolve leA_refl : core.
+  #[local]
   Hint Immediate eqA_dec leA_dec leA_antisym : core.
 
   Let emptyBag := EmptyBag A.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 2f445c341a..45fb48ad5d 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -76,6 +76,7 @@ Qed.
 
 End Permutation.
 
+#[global]
 Hint Resolve Permutation_refl perm_nil perm_skip : core.
 
 (* These hints do not reduce the size of the problem to solve and they
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 8cba461082..206eb606d2 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -137,7 +137,9 @@ Section defs.
 
 End defs.
 
+#[global]
 Hint Constructors HdRel : core.
+#[global]
 Hint Constructors Sorted : core.
 
 (* begin hide *)