Explicitly annotate all hint declarations of the standard library.

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

1 files changed, 2 insertions, 0 deletions

diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index 0f62a9419b..aa0c419f0e 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -466,6 +466,7 @@ the above form:
     (** Here is the tactic that will throw away hypotheses that
         are not useful (for the intended scope of the [fsetdec]
         tactic). *)
+    #[global]
     Hint Constructors MSet_elt_Prop MSet_Prop : MSet_Prop.
     Ltac discard_nonMSet :=
       repeat (
@@ -518,6 +519,7 @@ the above form:
 
     (** The hint database [MSet_decidability] will be given to
         the [push_neg] tactic from the module [Negation]. *)
+    #[global]
     Hint Resolve dec_In dec_eq : MSet_decidability.
 
     (** ** Normalizing Propositions About Equality