_CoqProject, meta, theories/dune

coq-community · Feb 5, 2025 · 8ff6c2d · 8ff6c2d
1 parent b45581a
commit 8ff6c2d
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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))