From 8ff6c2d5f2cc9e0bde3cc961baae1d7411cf9494 Mon Sep 17 00:00:00 2001
From: Damien Pous <damien.pous@ens-lyon.fr>
Date: Wed, 5 Feb 2025 22:25:06 +0100
Subject: [PATCH] _CoqProject, meta, theories/dune

---
 _CoqProject   | 2 +-
 meta.yml      | 2 +-
 theories/dune | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index cf13fea..efbd4c6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,7 +4,7 @@
 -I src
 
 -arg -w -arg +default
--arg -w -arg -deprecated-from-Coq
+# -arg -w -arg -deprecated-from-Coq
 
 src/coq.mli
 src/helper.mli
diff --git a/meta.yml b/meta.yml
index 42b1370..32aa2aa 100644
--- a/meta.yml
+++ b/meta.yml
@@ -82,7 +82,7 @@ documentation: |
   ```coq
   From AAC_tactics Require Import AAC.
   From AAC_tactics Require Instances.
-  From Coq Require Import ZArith.
+  From Stdlib Require Import ZArith.
 
   Section ZOpp.
     Import Instances.Z.
diff --git a/theories/dune b/theories/dune
index cecf9e7..6a50ba7 100644
--- a/theories/dune
+++ b/theories/dune
@@ -2,5 +2,5 @@
  (name AAC_tactics)
  (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)
+ (plugins coq-aac-tactics.plugin)
  (flags :standard -w +default))