diff --git a/extra-dev/packages/coq-mathcomp-boot/coq-mathcomp-boot.dev/opam b/extra-dev/packages/coq-mathcomp-boot/coq-mathcomp-boot.dev/opam
new file mode 100644
index 0000000000000000000000000000000000000000..1eb664ab26a16420b63fbaebb168d9be179cb74e
--- /dev/null
+++ b/extra-dev/packages/coq-mathcomp-boot/coq-mathcomp-boot.dev/opam
@@ -0,0 +1,16 @@
+opam-version: "2.0"
+version: "dev"
+maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+
+homepage: "https://math-comp.github.io/"
+bug-reports: "https://github.com/math-comp/math-comp/issues"
+dev-repo: "git+https://github.com/math-comp/math-comp.git"
+license: "CECILL-B"
+
+depends: [
+  "coq-core"
+  "rocq-mathcomp-boot" {= version}
+]
+authors: [ "The Mathematical Components team" ]
+
+synopsis: "Compatibility package for rocq-mathcomp-boot"
diff --git a/extra-dev/packages/coq-mathcomp-order/coq-mathcomp-order.dev/opam b/extra-dev/packages/coq-mathcomp-order/coq-mathcomp-order.dev/opam
new file mode 100644
index 0000000000000000000000000000000000000000..89d6baae9f443bed38de7da27a90284cf1354b65
--- /dev/null
+++ b/extra-dev/packages/coq-mathcomp-order/coq-mathcomp-order.dev/opam
@@ -0,0 +1,13 @@
+opam-version: "2.0"
+version: "dev"
+maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+
+homepage: "https://math-comp.github.io/"
+bug-reports: "https://github.com/math-comp/math-comp/issues"
+dev-repo: "git+https://github.com/math-comp/math-comp.git"
+license: "CECILL-B"
+
+depends: [ "rocq-mathcomp-order" {= version} ]
+authors: [ "The Mathematical Components team" ]
+
+synopsis: "Compatibility package for rocq-mathcomp-order"
diff --git a/extra-dev/packages/rocq-mathcomp-algebra/rocq-mathcomp-algebra.dev/opam b/extra-dev/packages/rocq-mathcomp-algebra/rocq-mathcomp-algebra.dev/opam
index 88f46151570acdf84f5878bf81d6293af9462151..6e2364788f8fe9932e90e3624e6e450a61ec6b8f 100644
--- a/extra-dev/packages/rocq-mathcomp-algebra/rocq-mathcomp-algebra.dev/opam
+++ b/extra-dev/packages/rocq-mathcomp-algebra/rocq-mathcomp-algebra.dev/opam
@@ -9,7 +9,10 @@ license: "CECILL-B"
 
 build: [ make "-C" "algebra" "-j" "%{jobs}%" ]
 install: [ make "-C" "algebra" "install" ]
-depends: [ "rocq-mathcomp-fingroup" { = version } ]
+depends: [
+  "rocq-mathcomp-order" { = version }
+  "rocq-mathcomp-fingroup" { = version }
+]
 
 tags: [
   "keyword:small scale reflection"
diff --git a/extra-dev/packages/rocq-mathcomp-boot/rocq-mathcomp-boot.dev/opam b/extra-dev/packages/rocq-mathcomp-boot/rocq-mathcomp-boot.dev/opam
new file mode 100644
index 0000000000000000000000000000000000000000..c8b83d4537a4be495218492057f03f1c6fd8d7fa
--- /dev/null
+++ b/extra-dev/packages/rocq-mathcomp-boot/rocq-mathcomp-boot.dev/opam
@@ -0,0 +1,52 @@
+opam-version: "2.0"
+version: "dev"
+maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+
+homepage: "https://math-comp.github.io/"
+bug-reports: "https://github.com/math-comp/math-comp/issues"
+dev-repo: "git+https://github.com/math-comp/math-comp.git"
+license: "CECILL-B"
+
+build: [ make "-C" "boot" "-j" "%{jobs}%" ]
+install: [ make "-C" "boot" "install" ]
+depends: [
+  ("coq" {>= "8.20" & < "8.21~"}
+  | "rocq-core" {>= "9.0" | = "dev"})
+  # Please keep the "dev" above as it is required for the coq-dev Docker images
+  "elpi" {>= "1.17.0"}
+  "rocq-hierarchy-builder" {>= "1.9.0"}
+]
+
+tags: [
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "keyword:bigop"
+  "keyword:big operators"
+  "keyword:biomial coefficient"
+  "keyword:integer division theory"
+  "keyword:finite sets"
+  "keyword:functions with finite domain"
+  "keyword:finite graphs"
+  "keyword:quotient types"
+  "keyword:lists"
+  "keyword:ordering and sorting lists"
+  "keyword:prime numbers"
+  "keyword:tuples"
+  "keyword:bounded lists"
+  "logpath:mathcomp.boot"
+]
+authors: [ "The Mathematical Components team" ]
+
+synopsis: "Small Scale Reflection"
+description: """
+This library includes the small scale reflection proof language
+extension and the minimal set of libraries to take advantage of it.
+This includes libraries on lists (seq), boolean and boolean
+predicates, natural numbers and types with decidable equality,
+finite types, finite sets, finite functions, finite graphs, basic arithmetics
+and prime numbers, big operators
+"""
+
+url {
+  src: "git+https://github.com/math-comp/math-comp.git#master"
+}
diff --git a/extra-dev/packages/rocq-mathcomp-order/rocq-mathcomp-order.dev/opam b/extra-dev/packages/rocq-mathcomp-order/rocq-mathcomp-order.dev/opam
new file mode 100644
index 0000000000000000000000000000000000000000..0539fd03581f68a593e2d9b0a7d65be36f7603e2
--- /dev/null
+++ b/extra-dev/packages/rocq-mathcomp-order/rocq-mathcomp-order.dev/opam
@@ -0,0 +1,33 @@
+opam-version: "2.0"
+version: "dev"
+maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+
+homepage: "https://math-comp.github.io/"
+bug-reports: "https://github.com/math-comp/math-comp/issues"
+dev-repo: "git+https://github.com/math-comp/math-comp.git"
+license: "CECILL-B"
+
+build: [ make "-C" "order" "-j" "%{jobs}%" ]
+install: [ make "-C" "order" "install" ]
+depends: [ "rocq-mathcomp-boot" { = version } ]
+
+tags: [
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "keyword:order theory"
+  "keyword:partial order"
+  "keyword:lattices"
+  "keyword:total order"
+  "logpath:mathcomp.order"
+]
+authors: [ "The Mathematical Components team" ]
+
+synopsis: "Mathematical Components Library on order theory"
+description: """
+This library contains definitions and theorems about partial orders,
+lattices, total orders...
+"""
+
+url {
+  src: "git+https://github.com/math-comp/math-comp.git#master"
+}
diff --git a/extra-dev/packages/rocq-mathcomp-ssreflect/rocq-mathcomp-ssreflect.dev/opam b/extra-dev/packages/rocq-mathcomp-ssreflect/rocq-mathcomp-ssreflect.dev/opam
index 83c7bb08f846c8755a71908f6603d2e70c0d00f2..616f319ef363a7c38ec6c439a5f928102688e243 100644
--- a/extra-dev/packages/rocq-mathcomp-ssreflect/rocq-mathcomp-ssreflect.dev/opam
+++ b/extra-dev/packages/rocq-mathcomp-ssreflect/rocq-mathcomp-ssreflect.dev/opam
@@ -10,45 +10,13 @@ license: "CECILL-B"
 build: [ make "-C" "ssreflect" "-j" "%{jobs}%" ]
 install: [ make "-C" "ssreflect" "install" ]
 depends: [
-  ("coq" {>= "8.19" & < "8.21~"}
-  | "rocq-core" {>= "9.0" | = "dev"})
-  # Please keep the "dev" above as it is required for the coq-dev Docker images
-  "elpi" {>= "1.17.0"}
-  "coq-hierarchy-builder" { >= "1.7.0"}
+  "rocq-mathcomp-boot" { = version }
+  "rocq-mathcomp-order" { = version }
 ]
 
-tags: [
-  "keyword:small scale reflection"
-  "keyword:mathematical components"
-  "keyword:bigop"
-  "keyword:big operators"
-  "keyword:biomial coefficient"
-  "keyword:integer division theory"
-  "keyword:finite sets"
-  "keyword:functions with finite domain"
-  "keyword:finite graphs"
-  "keyword:quotient types"
-  "keyword:order theory"
-  "keyword:partial order"
-  "keyword:lattices"
-  "keyword:lists"
-  "keyword:ordering and sorting lists"
-  "keyword:prime numbers"
-  "keyword:tuples"
-  "keyword:bounded lists"
-  "logpath:mathcomp.ssreflect"
-]
 authors: [ "The Mathematical Components team" ]
 
-synopsis: "Small Scale Reflection"
-description: """
-This library includes the small scale reflection proof language
-extension and the minimal set of libraries to take advantage of it.
-This includes libraries on lists (seq), boolean and boolean
-predicates, natural numbers and types with decidable equality,
-finite types, finite sets, finite functions, finite graphs, basic arithmetics
-and prime numbers, big operators
-"""
+synopsis: "Compatibility package for rocq-mathcomp-boot and rocq-mathcomp-order"
 
 url {
   src: "git+https://github.com/math-comp/math-comp.git#master"