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, 5 insertions, 0 deletions

diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index a154a2b269..3799ffaca9 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -279,27 +279,32 @@ Section SCANNING.
 Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop :=
  |Forall_nil: Forall P []
  |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v).
+#[local]
 Hint Constructors Forall : core.
 
 Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop :=
  |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v)
  |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v).
+#[local]
 Hint Constructors Exists : core.
 
 Inductive In {A} (a:A): forall {n}, t A n -> Prop :=
  |In_cons_hd {m} (v: t A m): In a (a::v)
  |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v).
+#[local]
 Hint Constructors In : core.
 
 Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
  |Forall2_nil: Forall2 P [] []
  |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 ->
     Forall2 P (x1::v1) (x2::v2).
+#[local]
 Hint Constructors Forall2 : core.
 
 Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
  |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2)
  |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2).
+#[local]
 Hint Constructors Exists2 : core.
 
 End SCANNING.