diff --git a/sci-mathematics/coq/coq-8.17.1-r1.ebuild b/sci-mathematics/coq/coq-8.17.1-r1.ebuild
index 0376c24fc404c..3c164c844d9be 100644
--- a/sci-mathematics/coq/coq-8.17.1-r1.ebuild
+++ b/sci-mathematics/coq/coq-8.17.1-r1.ebuild
@@ -9,8 +9,9 @@ MY_P="${PN}-${MY_PV}"
 inherit check-reqs desktop dune edo
 
 DESCRIPTION="Proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/
-	https://github.com/coq/coq/"
+HOMEPAGE="https://rocq-prover.org
+	https://github.com/rocq-prover/rocq/"
+
 SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz
 	-> ${P}.tar.gz"
 S="${WORKDIR}/${MY_P}"
diff --git a/sci-mathematics/coq/coq-8.19.2-r1.ebuild b/sci-mathematics/coq/coq-8.19.2-r1.ebuild
index 9613fc3a4f840..6b46ef0f3a4a0 100644
--- a/sci-mathematics/coq/coq-8.19.2-r1.ebuild
+++ b/sci-mathematics/coq/coq-8.19.2-r1.ebuild
@@ -9,8 +9,9 @@ MY_P="${PN}-${MY_PV}"
 inherit check-reqs desktop dune edo
 
 DESCRIPTION="Proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/
-	https://github.com/coq/coq/"
+HOMEPAGE="https://rocq-prover.org
+	https://github.com/rocq-prover/rocq/"
+
 SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz
 	-> ${P}.tar.gz"
 S="${WORKDIR}/${MY_P}"
diff --git a/sci-mathematics/coq/coq-8.20.0-r1.ebuild b/sci-mathematics/coq/coq-8.20.0-r1.ebuild
index 1c69a8de9461a..c1bd2a1ba3371 100644
--- a/sci-mathematics/coq/coq-8.20.0-r1.ebuild
+++ b/sci-mathematics/coq/coq-8.20.0-r1.ebuild
@@ -6,8 +6,8 @@ EAPI=8
 inherit check-reqs desktop dune edo
 
 DESCRIPTION="Proof assistant written in O'Caml"
-HOMEPAGE="https://coq.inria.fr/
-	https://github.com/coq/coq/"
+HOMEPAGE="https://rocq-prover.org
+	https://github.com/rocq-prover/rocq/"
 
 if [[ "${PV}" == *9999* ]] ; then
 	inherit git-r3
diff --git a/sci-mathematics/coq/coq-9.0.0.ebuild b/sci-mathematics/coq/coq-9.0.0.ebuild
index ac81887a2d4a0..09bf3909c962c 100644
--- a/sci-mathematics/coq/coq-9.0.0.ebuild
+++ b/sci-mathematics/coq/coq-9.0.0.ebuild
@@ -6,8 +6,8 @@ EAPI=8
 inherit check-reqs desktop dune edo
 
 DESCRIPTION="Coq/Rocq is a proof assistant written in O'Caml"
-HOMEPAGE="https://coq.inria.fr/
-	https://github.com/coq/coq/"
+HOMEPAGE="https://rocq-prover.org
+	https://github.com/rocq-prover/rocq/"
 
 if [[ "${PV}" == *9999* ]] ; then
 	inherit git-r3
diff --git a/sci-mathematics/coq/coq-9.1.0-r1.ebuild b/sci-mathematics/coq/coq-9.1.0-r1.ebuild
index 21b7bffc808eb..ac9ad6e10d8fa 100644
--- a/sci-mathematics/coq/coq-9.1.0-r1.ebuild
+++ b/sci-mathematics/coq/coq-9.1.0-r1.ebuild
@@ -6,8 +6,8 @@ EAPI=8
 inherit check-reqs desktop dune edo
 
 DESCRIPTION="Coq/Rocq is a proof assistant written in O'Caml"
-HOMEPAGE="https://coq.inria.fr/
-	https://github.com/coq/coq/"
+HOMEPAGE="https://rocq-prover.org
+	https://github.com/rocq-prover/rocq/"
 
 if [[ "${PV}" == *9999* ]] ; then
 	inherit git-r3
diff --git a/sci-mathematics/coq/metadata.xml b/sci-mathematics/coq/metadata.xml
index 3e812d4a672de..6c71a7b571663 100644
--- a/sci-mathematics/coq/metadata.xml
+++ b/sci-mathematics/coq/metadata.xml
@@ -1,33 +1,34 @@
 <?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>
-	<longdescription>
-	Developed in the LogiCal project, the Coq tool is a formal proof
-	management system: a proof done with Coq is mechanically checked
-	by the machine.
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <longdescription>
+    Developed in the LogiCal project, the Coq tool is a formal proof
+    management system: a proof done with Coq is mechanically checked
+    by the machine.
 
-	In particular, Coq allows:
-	* the definition of functions or predicates,
-	* to state mathematical theorems and software specifications,
-	* to develop interactively formal proofs of these theorems,
-	* to check these proofs by a small certification "kernel".
+    In particular, Coq allows:
+    * the definition of functions or predicates,
+    * to state mathematical theorems and software specifications,
+    * to develop interactively formal proofs of these theorems,
+    * to check these proofs by a small certification "kernel".
 
-	Coq is based on a logical framework called "Calculus of Inductive
-	Constructions" extended by a modular development system for
-	theories.
-	</longdescription>
-	<upstream>
-		<changelog>https://github.com/coq/coq/releases/</changelog>
-		<bugs-to>https://github.com/coq/coq/issues/</bugs-to>
-		<remote-id type="github">coq/coq</remote-id>
-	</upstream>
-	<use>
-		<flag name="native-compiler">
-			Enable "native_compute" and compile the Coq Standard Library
-		</flag>
-	</use>
+    Coq is based on a logical framework called "Calculus of Inductive
+    Constructions" extended by a modular development system for
+    theories.
+  </longdescription>
+  <upstream>
+    <changelog>https://github.com/rocq-prover/rocq/releases/</changelog>
+    <bugs-to>https://github.com/rocq-prover/rocq/issues/</bugs-to>
+    <remote-id type="github">rocq-prover/rocq</remote-id>
+  </upstream>
+  <use>
+    <flag name="native-compiler">
+      Enable "native_compute" and compile the Coq Standard Library
+    </flag>
+  </use>
 </pkgmetadata>