From 2b29e58067728852a069c591f0dd1493da8cb546 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 26 May 2019 10:09:19 +0200
Subject: [PATCH] remove unnecessary disabled warning

---
 _CoqProject | 2 --
 1 file changed, 2 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 08d3f0d..53bfb6e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,8 +6,6 @@
 -arg -w -arg -redundant-canonical-projection
 # change_no_check does not exist yet in 8.9.
 -arg -w -arg -convert_concl_no_check
-# "Declare Scope" does not exist yet in 8.9.
--arg -w -arg -undeclared-scope
 
 theories/barrier/proof.v
 theories/barrier/specification.v
-- 
GitLab