diff --git a/srcpkgs/rocq/patches/libdir.patch b/srcpkgs/rocq/patches/libdir.patch
new file mode 100644
index 00000000000..963895ec612
--- /dev/null
+++ b/srcpkgs/rocq/patches/libdir.patch
@@ -0,0 +1,12 @@
+--- a/tools/configure/configure.ml
++++ b/tools/configure/configure.ml
+@@ -392,7 +392,7 @@
+   pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n";
+   pr "(* Exact command that generated this file: *)\n";
+   pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv));
+-  pr_s "install_prefix" install_prefix;
++  pr_s "install_prefix" "/usr"; let _ = install_prefix in ();
+-  pr_s "coqlib" coqlib;
++  pr_s "coqlib" "/usr/lib/coq"; let _ = coqlib in ();
+   pr_s "configdir" configdir;
+   pr_s "datadir" datadir;
diff --git a/srcpkgs/coq/template b/srcpkgs/rocq/template
similarity index 57%
rename from srcpkgs/coq/template
rename to srcpkgs/rocq/template
index 0b5b19396cb..4f59321a5ba 100644
--- a/srcpkgs/coq/template
+++ b/srcpkgs/rocq/template
@@ -1,24 +1,20 @@
-# Template file for 'coq'
-pkgname=coq
-version=8.19.2
-revision=2
+# Template file for 'rocq'
+pkgname=rocq
+version=9.0.0
+revision=1
 hostmakedepends="dune ocaml ocaml-findlib ocaml-num ocaml-zarith"
 depends="ocaml-findlib"
 checkdepends="python3 rsync time"
 short_desc="Proof assistant written in OCaml"
 maintainer="Orphaned <orphan@voidlinux.org>"
 license="LGPL-2.1-only"
-homepage="https://coq.inria.fr"
-distfiles="https://github.com/coq/coq/archive/V${version}.tar.gz"
-checksum=18035624bcda4f8cffe5f348e02f0ae2503af1c40de165788d7d45578e6c5725
+homepage="https://rocq-prover.org/"
+distfiles="https://github.com/rocq-prover/rocq/releases/download/V${version}/rocq-${version}.tar.gz"
+checksum=82f86646fd3d047f760837648195c73374beee667b1c9592d31c5426e3b43a51
 nopie=yes
 nocross=yes
 make_check=ci-skip  # takes long and has some faults
-
-case "$XBPS_TARGET_MACHINE" in
-	ppc64*) ;;
-	ppc*) broken="R_PPC_REL24 relocation out of range";;
-esac
+replaces="coq>=0"
 
 do_patch() {
 	if ! command -v ocamlc.opt >/dev/null; then
@@ -29,11 +25,11 @@ do_patch() {
 
 do_build() {
 	make dunestrap
-	dune build --display=short -p coq-core,coq-stdlib,coqide-server
+	dune build --display=short -p rocq-core,rocq-runtime,coqide-server,coq-core
 }
 
 do_install() {
-	dune install coq-core coq-stdlib coqide-server --prefix=/usr --destdir="$DESTDIR" \
+	dune install rocq-core rocq-runtime coqide-server coq-core --prefix=/usr --destdir="$DESTDIR" \
 		--mandir=/usr/share/man --docdir=/usr/share/doc
 }