diff --git a/core-dev/packages/coq-core/coq-core.dev/opam b/core-dev/packages/coq-core/coq-core.dev/opam
new file mode 100644
index 0000000000..cee04e7809
--- /dev/null
+++ b/core-dev/packages/coq-core/coq-core.dev/opam
@@ -0,0 +1,43 @@
+opam-version: "2.0"
+maintainer: "coqdev@inria.fr"
+authors: "The Coq development team, INRIA, CNRS, and contributors."
+homepage: "https://coq.inria.fr/"
+bug-reports: "https://github.com/coq/coq/issues"
+dev-repo: "git+https://github.com/coq/coq.git"
+license: "LGPL-2.1-only"
+synopsis: "Formal proof management system"
+description: """
+The Coq proof assistant provides a formal language to write
+mathematical definitions, executable algorithms, and theorems, together
+with an environment for semi-interactive development of machine-checked
+proofs. Typical applications include the certification of properties of programming
+languages (e.g., the CompCert compiler certification project and the
+Bedrock verified low-level programming library), the formalization of
+mathematics (e.g., the full formalization of the Feit-Thompson theorem
+and homotopy type theory) and teaching.
+"""
+
+depopts: [
+  "coq-native"
+]
+
+depends: [
+  "ocaml" {>= "4.05.0"}
+  "ocamlfind" {build}
+  "dune" {>= "2.9.1"}
+  "conf-findutils" {build}
+  "zarith" {>= "1.10"}
+]
+
+build: [
+  [
+    "./configure"
+    "-prefix" prefix
+    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+  ]
+  [ "dune" "build" "-p" name "-j"  jobs ]
+]
+
+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
new file mode 100644
index 0000000000..368406d7dd
--- /dev/null
+++ b/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam
@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "coqdev@inria.fr"
+authors: "The Coq development team, INRIA, CNRS, and contributors."
+homepage: "https://coq.inria.fr/"
+bug-reports: "https://github.com/coq/coq/issues"
+dev-repo: "git+https://github.com/coq/coq.git"
+license: "LGPL-2.1-only"
+synopsis: "Formal proof management system"
+description: """
+The Coq proof assistant provides a formal language to write
+mathematical definitions, executable algorithms, and theorems, together
+with an environment for semi-interactive development of machine-checked
+proofs. Typical applications include the certification of properties of programming
+languages (e.g., the CompCert compiler certification project and the
+Bedrock verified low-level programming library), the formalization of
+mathematics (e.g., the full formalization of the Feit-Thompson theorem
+and homotopy type theory) and teaching.
+"""
+
+depopts: [
+  "coq-native"
+]
+
+depends: [
+  "ocaml" {>= "4.05.0"}
+  "ocamlfind" {build}
+  "dune" {>= "2.9.1"}
+  "conf-findutils" {build}
+  "zarith" {>= "1.10"}
+  "coq-core" {= version}
+]
+
+build: [
+  # This is akin to a configure step
+  [ "sed '1 a (mode native)' theories/dune" {coq-native:installed} ]
+  [ "dune" "build" "-p" name "-j"  jobs ]
+]
+
+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 86b4c426f4..0af9685143 100644
--- a/core-dev/packages/coq/coq.dev/opam
+++ b/core-dev/packages/coq/coq.dev/opam
@@ -20,29 +20,10 @@ and homotopy type theory) and teaching.
 depopts: [
   "coq-native"
 ]
+
 depends: [
-  "ocaml" {>= "4.05.0"}
-  "ocamlfind" {build}
-  "dune" {>= "2.5.1"}
-  "conf-findutils" {build}
-  "zarith" {>= "1.10"}
-]
-build: [
-  [
-    "./configure"
-    "-configdir" "%{lib}%/coq/config"
-    "-prefix" prefix
-    "-mandir" man
-    "-docdir" doc
-    "-libdir" "%{lib}%/coq"
-    "-datadir" "%{share}%/coq"
-    "-coqide" "no"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
-  ]
-  [make "-j%{jobs}%"]
-]
-install: [
-  [make "install"]
+  "coq-core" {= version}
+  "coq-stdlib" {= version}
 ]
 
 url {