From 71cf8457314bcb6e59505825fb58fd6f9b260163 Mon Sep 17 00:00:00 2001
From: Anton Trunov <anton@zilliqa.com>
Date: Wed, 12 Aug 2020 20:43:37 +0300
Subject: [PATCH] Remove the option turning warnings into errors

This is because when Coq's master branch introduces new warnings
lemma-overloading causes Coq\'s CI to fail
---
 CHANGELOG.md  | 2 ++
 README.md     | 1 -
 _CoqProject   | 1 -
 theories/dune | 1 -
 4 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bfb1bed..4db5372 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,8 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ## [Unreleased]
+### Changed
+- Remove the option turning warnings into errors
 
 ## [8.12.0] - 2020-08-12
 ### Added
diff --git a/README.md b/README.md
index 49296e1..c189f77 100644
--- a/README.md
+++ b/README.md
@@ -41,7 +41,6 @@ re-implementations for comparison.
   - Beta Ziliani (initial)
   - Aleksandar Nanevski (initial)
   - Derek Dreyer (initial)
-
 - Coq-community maintainer(s):
   - Anton Trunov ([**@anton-trunov**](https://github.com/anton-trunov))
 - License: [GNU General Public License v3.0 or later](LICENSE.md)
diff --git a/_CoqProject b/_CoqProject
index 4b7f97d..6a49a02 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,5 @@
 -Q theories LemmaOverloading
 
--arg -w -arg +default
 -arg -w -arg -notation-overridden
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
diff --git a/theories/dune b/theories/dune
index a6da99c..51c50c9 100644
--- a/theories/dune
+++ b/theories/dune
@@ -3,7 +3,6 @@
  (package coq-lemma-overloading)
  (synopsis "Libraries demonstrating design patterns for programming and proving with canonical structures in Coq")
  (flags
-   -w +default
    -w -notation-overridden
    -w -projection-no-head-constant
    -w -redundant-canonical-projection