Merge pull request #79 from Alizter/dune-3-8

dune: bump to 3.8
math-comp · Nov 30, 2023 · 4c8c7e9 · 4c8c7e9
2 parents 9893f5f + b661f0e
commit 4c8c7e9
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 131 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,4 +1,3 @@
 /attic/
 /_build/
-/src/dune
 *~
diff --git a/configure b/configure
diff --git a/coq-mathcomp-multinomials.opam b/coq-mathcomp-multinomials.opam
@@ -6,12 +6,11 @@ dev-repo: "git+https://github.com/math-comp/multinomials.git"
 license: "CECILL-B"
 authors: ["Pierre-Yves Strub"]
 build: [
-  [ "bash" "./configure" ]
   [ "dune" "build" "-p" name "-j" jobs ]
 ]
 depends: [
   "coq"                    {(>= "8.16" & < "8.19~") | = "dev"}
-  "dune"                   {>= "2.8"}
+  "dune"                   {>= "3.8"}
   "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.2~") | = "dev"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-bigenough" {(>= "1.0" & < "1.1~") | = "dev"}

diff --git a/dune-project b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.8)
-(using coq 0.3)
+(lang dune 3.8)
+(using coq 0.8)
 (name multinomials)
diff --git a/src/dune b/src/dune
@@ -0,0 +1,16 @@
+(coq.theory
+ (name mathcomp.multinomials)
+ (package coq-mathcomp-multinomials)
+ (flags
+  -w -ambiguous-paths
+  -w -notation-overridden
+  -w -redundant-canonical-projection
+  -w -projection-no-head-constant)
+ (theories
+  elpi
+  HB
+  mathcomp.ssreflect
+  mathcomp.fingroup
+  mathcomp.algebra
+  mathcomp.bigenough
+  mathcomp.finmap))
diff --git a/src/dune.in b/src/dune.in