diff --git a/core-dev/packages/coq-core/coq-core.dev/opam b/core-dev/packages/coq-core/coq-core.dev/opam
index 100cea7076..ee3c537132 100644
--- a/core-dev/packages/coq-core/coq-core.dev/opam
+++ b/core-dev/packages/coq-core/coq-core.dev/opam
@@ -1,6 +1,4 @@
-# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "dev"
 synopsis: "The Coq Proof Assistant -- Core Binaries and Tools"
 description: """
 Coq is a formal proof management system. It provides
@@ -31,14 +29,15 @@ depends: [
   "ocaml" {>= "4.09.0"}
   "ocamlfind" {>= "1.8.1"}
   "zarith" {>= "1.11"}
-  "ounit2" {with-test}
+  "odoc" {with-doc}
 ]
 conflicts: [
   "coq"   { < "8.17" }
 ]
+depopts: ["coq-native"]
+dev-repo: "git+https://github.com/coq/coq.git"
 build: [
-  # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219
-  # ["dune" "subst"] {pinned}
+  ["dune" "subst"] {dev}
   [ "./configure"
     "-prefix" prefix
     "-mandir" man
@@ -52,13 +51,13 @@ build: [
     name
     "-j"
     jobs
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
-dev-repo: "git+https://github.com/coq/coq.git"
-depopts: ["coq-native"]
 
 url {
   src: "git+https://github.com/coq/coq.git#master"
diff --git a/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam b/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam
index 1f3b61c7e8..19d62a1529 100644
--- a/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam
+++ b/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam
@@ -1,6 +1,4 @@
-# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "dev"
 synopsis: "The Coq Proof Assistant -- Standard Library"
 description: """
 Coq is a formal proof management system. It provides
@@ -25,20 +23,14 @@ bug-reports: "https://github.com/coq/coq/issues"
 depends: [
   "dune" {>= "2.9"}
   "coq-core" {= version}
+  "odoc" {with-doc}
 ]
+depopts: ["coq-native"]
+dev-repo: "git+https://github.com/coq/coq.git"
 build: [
-  # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219
-  # ["dune" "subst"] {pinned}
-  #
-  # XXX need to run configure as in coq-core, or else dunestrap will
-  # use the default rule in config
-  [ "./configure"
-    "-prefix" prefix
-    "-mandir" man
-    "-libdir" "%{lib}%/coq"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
-  ]
-  [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ]
+  ["dune" "subst"] {dev}
+  # We tell dunestrap to use coq-config from coq-core
+  [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" "DUNESTRAPOPT=-p coq-stdlib"]
   [
     "dune"
     "build"
@@ -46,13 +38,13 @@ build: [
     name
     "-j"
     jobs
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
-dev-repo: "git+https://github.com/coq/coq.git"
-depopts: ["coq-native"]
 
 url {
   src: "git+https://github.com/coq/coq.git#master"
diff --git a/core-dev/packages/coq/coq.dev/opam b/core-dev/packages/coq/coq.dev/opam
index f9f5adcf88..f147f15e74 100644
--- a/core-dev/packages/coq/coq.dev/opam
+++ b/core-dev/packages/coq/coq.dev/opam
@@ -1,6 +1,4 @@
-# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "dev"
 synopsis: "The Coq Proof Assistant"
 description: """
 Coq is a formal proof management system. It provides
@@ -24,9 +22,18 @@ depends: [
   "coq-core" {= version}
   "coq-stdlib" {= version}
   "coqide-server" {= version}
+  "ounit2" {with-test}
+  "odoc" {with-doc}
 ]
+dev-repo: "git+https://github.com/coq/coq.git"
 build: [
-  ["dune" "subst"] {pinned}
+  ["dune" "subst"] {dev}
+  [ "./configure"
+    "-prefix" prefix
+    "-mandir" man
+    "-libdir" "%{lib}%/coq"
+    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+  ] {with-test}
   [
     "dune"
     "build"
@@ -34,12 +41,13 @@ build: [
     name
     "-j"
     jobs
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
-dev-repo: "git+https://github.com/coq/coq.git"
 
 url {
   src: "git+https://github.com/coq/coq.git#master"
diff --git a/core-dev/packages/coqide-server/coqide-server.dev/opam b/core-dev/packages/coqide-server/coqide-server.dev/opam
index 9dabe533bb..92c8f50db3 100644
--- a/core-dev/packages/coqide-server/coqide-server.dev/opam
+++ b/core-dev/packages/coqide-server/coqide-server.dev/opam
@@ -10,8 +10,8 @@ This package provides the `coqidetop` language server, an
 implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
 which allows clients, such as CoqIDE, to interact with Coq in a
 structured way."""
-maintainer: "The Coq development team <coqdev@inria.fr>"
-authors: "The Coq development team, INRIA, CNRS, and contributors"
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
@@ -19,16 +19,23 @@ bug-reports: "https://github.com/coq/coq/issues"
 depends: [
   "dune" {>= "2.9"}
   "coq-core" {= version}
+  "odoc" {with-doc}
 ]
 build: [
-  "dune"
-  "build"
-  "-p"
-  name
-  "-j"
-  jobs
-  "@install"
-  "@doc" {with-doc}
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/coq/coq.git"