diff --git a/Makefile b/Makefile
index f79ab37..257ce2a 100644
--- a/Makefile
+++ b/Makefile
@@ -1,19 +1,25 @@
-# -*- Makefile -*-
+# KNOWNTARGETS will not be passed along to CoqMakefile
+KNOWNTARGETS := Makefile.coq
+# KNOWNFILES will not get implicit targets from the final rule, and so
+# depending on them won't invoke the submake
+# Warning: These files get declared as PHONY, so any targets depending
+# on them always get rebuilt
+KNOWNFILES   := Makefile _CoqProject
 
-# --------------------------------------------------------------------
-DUNEOPTS ?=
-DUNE     := dune $(DUNEOPTS)
+.DEFAULT_GOAL := invoke-coqmakefile
 
-# --------------------------------------------------------------------
-.PHONY: default build clean
+Makefile.coq: Makefile _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-default: build
+invoke-coqmakefile: Makefile.coq
+	$(MAKE) --no-print-directory -f Makefile.coq $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
 
-build:
-	$(DUNE) build
+.PHONY: invoke-coqmakefile $(KNOWNFILES)
 
-install:
-	$(DUNE) install
+####################################################################
+##                      Your targets here                         ##
+####################################################################
 
-clean:
-	$(DUNE) clean
+# This should be the last rule, to handle any targets not declared above
+%: invoke-coqmakefile
+	@true
diff --git a/_CoqProject b/_CoqProject
index e183c8f..59da9bc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,11 @@
+src/freeg.v
+src/monalg.v
+src/mpoly.v
+src/ssrcomplements.v
+src/xfinmap.v
+
+-R src mathcomp.multinomials
 -arg -w -arg -ambiguous-paths
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -projection-no-head-constant
-
--R _build/default/src mathcomp.multinomials
diff --git a/coq-mathcomp-multinomials.opam b/coq-mathcomp-multinomials.opam
index b50c7cc..6811722 100644
--- a/coq-mathcomp-multinomials.opam
+++ b/coq-mathcomp-multinomials.opam
@@ -5,12 +5,10 @@ bug-reports: "https://github.com/math-comp/multinomials/issues"
 dev-repo: "git+https://github.com/math-comp/multinomials.git"
 license: "CECILL-B"
 authors: ["Pierre-Yves Strub"]
-build: [
-  [ "dune" "build" "-p" name "-j" jobs ]
-]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
 depends: [
   "coq"                    {(>= "8.16" & < "8.20~") | = "dev"}
-  "dune"                   {>= "3.8"}
   "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.3~") | = "dev"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-bigenough" {(>= "1.0" & < "1.1~") | = "dev"}
diff --git a/dune-project b/dune-project
deleted file mode 100644
index 7848d5a..0000000
--- a/dune-project
+++ /dev/null
@@ -1,3 +0,0 @@
-(lang dune 3.8)
-(using coq 0.8)
-(name multinomials)
diff --git a/src/dune b/src/dune
deleted file mode 100644
index 753216f..0000000
--- a/src/dune
+++ /dev/null
@@ -1,17 +0,0 @@
-(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
-  elpi_elpi
-  HB
-  mathcomp.ssreflect
-  mathcomp.fingroup
-  mathcomp.algebra
-  mathcomp.bigenough
-  mathcomp.finmap))