From 353669f8f175adabf878be0334a1979c439778af Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 4 Jul 2022 15:49:04 +0200
Subject: Re-enable `deprecated-hint-rewrite-without-locality` warning

No longer triggered since commit df076edfe.
---
 Makefile | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 103a6cb3..0acfbed4 100644
--- a/Makefile
+++ b/Makefile
@@ -64,8 +64,7 @@ endif
 COQCOPTS ?= \
   -w -undeclared-scope \
   -w -unused-pattern-matching-variable \
-  -w -deprecated-ident-entry \
-  -w -deprecated-hint-rewrite-without-locality
+  -w -deprecated-ident-entry
 
 cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
 
-- 
cgit