diff --git a/sci-mathematics/coq-stdlib/Manifest b/sci-mathematics/coq-stdlib/Manifest
new file mode 100644
index 0000000000000..103968602d617
--- /dev/null
+++ b/sci-mathematics/coq-stdlib/Manifest
@@ -0,0 +1 @@
+DIST coq-stdlib-9.0.0.tar.gz 1826759 BLAKE2B de68fa0a1528d1ac9843e3b4b34b4e56beeca80d4f0c35f26a103fdf7dee2ed74395961f490d670720f05d40ebc0851a3e4f18bc6224330fd78c2874ecd273b1 SHA512 97faa80d63a398c2c6872e043d65b1b907bb01ec3ea42f35cf757b3457b8fa2b64475d1577000ce2dea2c3f93e59e36cc5af9864adacf47f92db96ecbe307a45
diff --git a/sci-mathematics/coq-stdlib/coq-stdlib-9.0.0.ebuild b/sci-mathematics/coq-stdlib/coq-stdlib-9.0.0.ebuild
new file mode 100644
index 0000000000000..d73a8ec27eb87
--- /dev/null
+++ b/sci-mathematics/coq-stdlib/coq-stdlib-9.0.0.ebuild
@@ -0,0 +1,45 @@
+# Copyright 1999-2025 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit dune
+
+DESCRIPTION="Stdlib for the Coq/Rocq Prover, used to be part of Coq"
+HOMEPAGE="https://github.com/coq/stdlib"
+
+if [[ "${PV}" == *9999* ]] ; then
+	inherit git-r3
+
+	EGIT_REPO_URI="https://github.com/coq/stdlib"
+else
+	SRC_URI="https://github.com/coq/stdlib/archive/V${PV}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}/stdlib-${PV}"
+
+	KEYWORDS="~amd64"
+fi
+
+LICENSE="LGPL-2.1"
+SLOT="0/${PV}"
+IUSE="+ocamlopt"
+
+DUNE_PACKAGES=(
+	coq-stdlib
+	rocq-stdlib
+)
+
+RDEPEND="
+	>=sci-mathematics/coq-${PV}
+"
+DEPEND="
+	${RDEPEND}
+"
+
+src_compile() {
+	dune-compile "${DUNE_PACKAGES[@]}"
+}
+
+src_install() {
+	dune-install "${DUNE_PACKAGES[@]}"
+}
diff --git a/sci-mathematics/coq-stdlib/metadata.xml b/sci-mathematics/coq-stdlib/metadata.xml
new file mode 100644
index 0000000000000..e72497feaa2d0
--- /dev/null
+++ b/sci-mathematics/coq-stdlib/metadata.xml
@@ -0,0 +1,14 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <upstream>
+    <changelog>https://github.com/coq/stdlib/releases/</changelog>
+    <bugs-to>https://github.com/coq/stdlib/issues/</bugs-to>
+    <remote-id type="github">coq/stdlib</remote-id>
+  </upstream>
+</pkgmetadata>