diff --git a/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam b/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam
new file mode 100644
index 0000000000..d4761a8b2a
--- /dev/null
+++ b/extra-dev/packages/coq-equations/coq-equations.1.3.1+9.0/opam
@@ -0,0 +1,11 @@
+opam-version: "2.0"
+authors: [ "Matthieu Sozeau <matthieu.sozeau@inria.fr>" ]
+maintainer: "matthieu.sozeau@inria.fr"
+homepage: "https://mattam82.github.io/Coq-Equations"
+dev-repo: "git+https://github.com/mattam82/Coq-Equations.git"
+bug-reports: "https://github.com/mattam82/Coq-Equations/issues"
+license: "LGPL-2.1-only"
+depends: [
+  "rocq-equations" { = "1.3.1+9.0" }
+]
+synopsis: "Compatibility package, see rocq-equations"
diff --git a/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam b/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam
new file mode 100644
index 0000000000..2896ade713
--- /dev/null
+++ b/extra-dev/packages/rocq-equations/rocq-equations.1.3.1+9.0/opam
@@ -0,0 +1,46 @@
+opam-version: "2.0"
+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."
+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"
+]
+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" {>= "9.0~" & != "dev" & != "9.0.dev" }
+  "coq" (* As dune coq lang relies on coq compatibility packages *)
+  "ppx_optcomp" {build}
+  "ocaml-lsp-server" {with-dev-setup}
+  "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/mattam82/Coq-Equations.git"
+url {
+  src: "https://github.com/mattam82/Coq-Equations/releases/download/v1.3.1-9.0/Coq-Equations-1.3.1-9.0.tar.gz"
+  checksum: "sha512=e8c4aa5b1ec4f9636b52047f0911c7bc7d3b69042011a626a8770866c7ca5f7cd722a45d62ff7ddf9903c4f295c7ca5cbe49f9e18f9675d55251f0e4c533306c"
+}
\ No newline at end of file