diff --git a/packages/coq-core/coq-core.8.20.1/opam b/packages/coq-core/coq-core.8.20.1/opam
new file mode 100644
index 00000000000..ae2fec22eff
--- /dev/null
+++ b/packages/coq-core/coq-core.8.20.1/opam
@@ -0,0 +1,69 @@
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant -- Core Binaries and Tools"
+description: """
+Coq is a formal proof management system. It 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, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package includes the Coq core binaries, plugins, and tools, but
+not the vernacular standard library.
+
+Note that in this setup, Coq needs to be started with the -boot and
+-noinit options, as will otherwise fail to find the regular Coq
+prelude, now living in the coq-stdlib package."""
+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/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "3.6.1"}
+  "ocaml" {>= "4.09.0"}
+  "ocamlfind" {>= "1.8.1"}
+  "zarith" {>= "1.11"}
+  "conf-linux-libc-dev" {os = "linux"}
+  "odoc" {with-doc}
+]
+conflicts: [
+  "coq"   { < "8.17" }
+]
+depopts: ["coq-native" "memprof-limits" "memtrace"]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["dune" "subst"] {dev}
+  [ "./configure"
+    "-prefix" prefix
+    "-mandir" man
+    "-libdir" "%{lib}%/coq"
+    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+  ]
+  [
+    "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]
+]
+
+url {
+  src: "https://github.com/coq/coq/releases/download/V8.20.1/coq-8.20.1.tar.gz"
+  checksum: [
+    "md5=0cfaa70f569be9494d24c829e6555d46"
+    "sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2"
+  ]
+}
diff --git a/packages/coq-stdlib/coq-stdlib.8.20.1/opam b/packages/coq-stdlib/coq-stdlib.8.20.1/opam
new file mode 100644
index 00000000000..bf602a82fc0
--- /dev/null
+++ b/packages/coq-stdlib/coq-stdlib.8.20.1/opam
@@ -0,0 +1,55 @@
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant -- Standard Library"
+description: """
+Coq is a formal proof management system. It 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, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package includes the Coq Standard Library, that is to say, the
+set of modules usually bound to the Coq.* namespace."""
+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/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "3.6"}
+  "coq-core" {= version}
+  "odoc" {with-doc}
+]
+depopts: ["coq-native"]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["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"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+
+url {
+  src: "https://github.com/coq/coq/releases/download/V8.20.1/coq-8.20.1.tar.gz"
+  checksum: [
+    "md5=0cfaa70f569be9494d24c829e6555d46"
+    "sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2"
+  ]
+}
diff --git a/packages/coq/coq.8.20.1/opam b/packages/coq/coq.8.20.1/opam
new file mode 100644
index 00000000000..bd5d7b7268c
--- /dev/null
+++ b/packages/coq/coq.8.20.1/opam
@@ -0,0 +1,50 @@
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant"
+description: """
+Coq is a formal proof management system. It 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, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching."""
+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/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "3.6"}
+  "coq-core" {= version}
+  "coq-stdlib" {= version}
+  "coqide-server" {= version}
+  "odoc" {with-doc}
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+
+url {
+  src: "https://github.com/coq/coq/releases/download/V8.20.1/coq-8.20.1.tar.gz"
+  checksum: [
+    "md5=0cfaa70f569be9494d24c829e6555d46"
+    "sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2"
+  ]
+}
diff --git a/packages/coqide-server/coqide-server.8.20.1/opam b/packages/coqide-server/coqide-server.8.20.1/opam
new file mode 100644
index 00000000000..6388f6433f7
--- /dev/null
+++ b/packages/coqide-server/coqide-server.8.20.1/opam
@@ -0,0 +1,46 @@
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant, XML protocol server"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+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"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "3.6"}
+  "coq-core" {= version}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+
+url {
+  src: "https://github.com/coq/coq/releases/download/V8.20.1/coq-8.20.1.tar.gz"
+  checksum: [
+    "md5=0cfaa70f569be9494d24c829e6555d46"
+    "sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2"
+  ]
+}