From 081c7c29feb1f4c2e66331a88c273f802c9bc27c Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 4 Mar 2021 22:56:43 +0100
Subject: Silence Hint Locality warning

---
 mathcomp/Make           | 1 +
 mathcomp/_CoqProject    | 1 +
 mathcomp/algebra/Make   | 1 +
 mathcomp/character/Make | 1 +
 mathcomp/field/Make     | 3 ++-
 mathcomp/fingroup/Make  | 3 ++-
 mathcomp/solvable/Make  | 3 ++-
 mathcomp/ssreflect/Make | 3 ++-
 8 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/mathcomp/Make b/mathcomp/Make
index 0ef0b23..bdcd60f 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -100,3 +100,4 @@ ssreflect/tuple.v
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +non-primitive-record
 -arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality
diff --git a/mathcomp/_CoqProject b/mathcomp/_CoqProject
index ca863b3..875e152 100644
--- a/mathcomp/_CoqProject
+++ b/mathcomp/_CoqProject
@@ -7,3 +7,4 @@
 -arg -w -arg +duplicate-clear
 -arg -w -arg +non-primitive-record
 -arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality
diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make
index 0d0629f..68ea194 100644
--- a/mathcomp/algebra/Make
+++ b/mathcomp/algebra/Make
@@ -26,3 +26,4 @@ zmodp.v
 -arg -w -arg +duplicate-clear
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality
diff --git a/mathcomp/character/Make b/mathcomp/character/Make
index b750b49..77d4640 100644
--- a/mathcomp/character/Make
+++ b/mathcomp/character/Make
@@ -15,3 +15,4 @@ vcharacter.v
 -arg -w -arg +duplicate-clear
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality
diff --git a/mathcomp/field/Make b/mathcomp/field/Make
index 93795e9..cde04b3 100644
--- a/mathcomp/field/Make
+++ b/mathcomp/field/Make
@@ -17,4 +17,5 @@ separable.v
 -arg -w -arg -notation-overridden
 -arg -w -arg +duplicate-clear
 -arg -w -arg -ambiguous-paths
--arg -w -arg +undeclared-scope
\ No newline at end of file
+-arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality
diff --git a/mathcomp/fingroup/Make b/mathcomp/fingroup/Make
index 0f25f14..6c16e9a 100644
--- a/mathcomp/fingroup/Make
+++ b/mathcomp/fingroup/Make
@@ -15,4 +15,5 @@ quotient.v
 -arg -w -arg -notation-overridden
 -arg -w -arg +duplicate-clear
 -arg -w -arg -ambiguous-paths
--arg -w -arg +undeclared-scope
\ No newline at end of file
+-arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality
diff --git a/mathcomp/solvable/Make b/mathcomp/solvable/Make
index 2f5aac3..51f4fdf 100644
--- a/mathcomp/solvable/Make
+++ b/mathcomp/solvable/Make
@@ -26,4 +26,5 @@ sylow.v
 -arg -w -arg -notation-overridden
 -arg -w -arg +duplicate-clear
 -arg -w -arg -ambiguous-paths
--arg -w -arg +undeclared-scope
\ No newline at end of file
+-arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index b909046..9174856 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -31,4 +31,5 @@ order.v
 -arg -w -arg +duplicate-clear
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +undeclared-scope
--arg -w -arg -non-reversible-notation
\ No newline at end of file
+-arg -w -arg -non-reversible-notation
+-arg -w -arg -deprecated-hint-without-locality
-- 
cgit v1.2.3