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/Wellfounded/Inclusion.v          | 1 +
 theories/Wellfounded/Transitive_Closure.v | 1 +
 2 files changed, 2 insertions(+)

(limited to 'theories/Wellfounded')

diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index 474836d53d..cafa849b1b 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -22,6 +22,7 @@ Section WfInclusion.
     apply Acc_intro; auto with sets.
   Qed.
 
+  #[local]
   Hint Resolve Acc_incl : core.
 
   Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 2d139504f3..49c2dd8602 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -31,6 +31,7 @@ Section Wf_Transitive_Closure.
     apply Acc_inv with y; auto with sets.
   Defined.
 
+  #[local]
   Hint Resolve Acc_clos_trans : core.
 
   Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y.
-- 
cgit v1.2.3