diff --git a/extra-dev/packages/rocq-equations/rocq-equations.dev/opam b/extra-dev/packages/rocq-equations/rocq-equations.dev/opam
index 26bb85139..2025754af 100644
--- a/extra-dev/packages/rocq-equations/rocq-equations.dev/opam
+++ b/extra-dev/packages/rocq-equations/rocq-equations.dev/opam
@@ -1,46 +1,45 @@
 opam-version: "2.0"
-authors: [ "Matthieu Sozeau <matthieu.sozeau@inria.fr>" "Cyprien Mangin <cyprien.mangin@m4x.org>" ]
-dev-repo: "git+https://github.com/mattam82/Coq-Equations.git"
-maintainer: "matthieu.sozeau@inria.fr"
-homepage: "https://mattam82.github.io/Coq-Equations"
-bug-reports: "https://github.com/mattam82/Coq-Equations/issues"
-license: "LGPL-2.1-only"
 synopsis: "A function definition package for Rocq"
-description: """
-Equations is a function definition plugin for Rocq, that allows the
-definition of functions by dependent pattern-matching and well-founded,
-mutual or nested structural recursion and compiles them into core
-terms. It automatically derives the clauses equations, the graph of the
-function and its associated elimination principle.
-"""
+description:
+  "Equations is a function definition plugin for Rocq, that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle."
+maintainer: ["Matthieu Sozeau <matthieu.sozeau@inria.fr>"]
+authors: [
+  "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
+  "Cyprien Mangin <cyprien.mangin@m4x.org>"
+]
+license: "LGPL-2.1-only"
 tags: [
   "keyword:dependent pattern-matching"
   "keyword:functional elimination"
   "category:Miscellaneous/Coq Extensions"
   "logpath:Equations"
 ]
-build: [
-  ["./configure.sh" "--enable-hott" {coq-hott:installed} ]
-  [make "-j%{jobs}%"]
-]
-install: [
-  [make "install"]
-]
-run-test: [
-  [make "test-suite"]
-]
+homepage: "https://mattam82.github.io/Coq-Equations"
+bug-reports: "https://github.com/mattam82/Coq-Equations/issues"
 depends: [
   "dune" {>= "3.13"}
   "ocaml" {>= "4.10.0"}
   "rocq-prover" { = "dev" }
-  "coq" { = "dev" }
+  "coq" (* As dune coq lang relies on coq compatibility packages *)
   "ppx_optcomp" {build}
   "ocaml-lsp-server" {with-dev-setup}
   "odoc" {with-doc}
 ]
-depopts: [
-  "coq-hott"
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
 ]
+dev-repo: "git+https://github.com/mattam82/Coq-Equations.git"
 url {
   src: "git+https://github.com/mattam82/Coq-Equations#main"
 }