From 956129a02ef295da01e0220c6b0d62c74fe1fa7a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 4 Jun 2025 12:28:05 -0400 Subject: [PATCH 1/2] Do not treat default warnings as errors in dune https://github.com/rocq-community/aac-tactics/pull/157#issuecomment-2935561812 --- theories/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/dune b/theories/dune index cecf9e7..77fa2b0 100644 --- a/theories/dune +++ b/theories/dune @@ -3,4 +3,4 @@ (package coq-aac-tactics) (synopsis "Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators") (libraries coq-aac-tactics.plugin) - (flags :standard -w +default)) + (flags :standard)) From e100ddc66790a02f27549fef120e6946ff3d76a1 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 4 Jun 2025 13:34:03 -0400 Subject: [PATCH 2/2] Update theories/dune MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Gaëtan Gilbert --- theories/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/dune b/theories/dune index 77fa2b0..164f039 100644 --- a/theories/dune +++ b/theories/dune @@ -3,4 +3,4 @@ (package coq-aac-tactics) (synopsis "Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators") (libraries coq-aac-tactics.plugin) - (flags :standard)) +)