From 103aa7074a9dd3b1bcb2864d52c89292a2ab7bff Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Mon, 19 Sep 2022 16:28:06 +0200
Subject: Add `Declare Scope` where appropriate (#440)

And re-enable the `undeclared-scope` warning.

`Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
---
 Makefile | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index b3b7a124..48648a0a 100644
--- a/Makefile
+++ b/Makefile
@@ -44,9 +44,6 @@ endif
 
 # Notes on silenced Coq warnings:
 #
-# undeclared-scope:
-#    warning introduced in 8.12
-#    suggested change (use `Declare Scope`) supported since 8.12
 # unused-pattern-matching-variable:
 #    warning introduced in 8.13
 #    the code rewrite that avoids the warning is not desirable
@@ -58,7 +55,6 @@ endif
 #    triggered by Menhir-generated files, to be solved upstream in Menhir
 
 COQCOPTS ?= \
-  -w -undeclared-scope \
   -w -unused-pattern-matching-variable \
   -w -deprecated-ident-entry
 
-- 
cgit