diff --git a/released/packages/coq-coqeal/coq-coqeal.2.1.0/opam b/released/packages/coq-coqeal/coq-coqeal.2.1.0/opam
index fdc8dbd7c5a218f7a21b75a03a70ebbbf3e74c18..508551619838384a4202e5a095427e5aadde6acd 100644
--- a/released/packages/coq-coqeal/coq-coqeal.2.1.0/opam
+++ b/released/packages/coq-coqeal/coq-coqeal.2.1.0/opam
@@ -21,7 +21,7 @@ depends: [
   "coq-bignums"
   "coq-elpi" {>= "2.5.0"}
   "coq-hierarchy-builder" {>= "1.4.0"}
-  "coq-mathcomp-ssreflect" {>= "2.3" & < "2.4~"}
+  "coq-mathcomp-ssreflect" {>= "2.3" & < "2.5~"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-multinomials" {>= "2.0"}
   "coq-mathcomp-real-closed" {>= "2.0"}
diff --git a/released/packages/coq-deriving/coq-deriving.0.2.1/opam b/released/packages/coq-deriving/coq-deriving.0.2.1/opam
index 5ea486a2aa9b8a66b0c7ed8ee5f3009b73f4d8f4..7679abdf80f0e44c44bb25716a16c7b0e56438ec 100644
--- a/released/packages/coq-deriving/coq-deriving.0.2.1/opam
+++ b/released/packages/coq-deriving/coq-deriving.0.2.1/opam
@@ -10,7 +10,7 @@ build: [ make "-j" "%{jobs}%" "test" {with-test} ]
 install: [ make "install" ]
 depends: [
   "coq" { (>= "8.17" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-mathcomp-ssreflect" {>= "2.0" & < "2.4~"}
 ]
 
 tags: [
diff --git a/released/packages/coq-extructures/coq-extructures.0.4.0/opam b/released/packages/coq-extructures/coq-extructures.0.4.0/opam
index 4c59de0e4a0b78078ef22109ac3c490c010af784..b3b1c3e7201e84ef3741d8a59711266eb47d61cb 100644
--- a/released/packages/coq-extructures/coq-extructures.0.4.0/opam
+++ b/released/packages/coq-extructures/coq-extructures.0.4.0/opam
@@ -15,7 +15,7 @@ install: [
 depends: [
   "ocaml"
   "coq" {(>= "8.17" & < "8.21~")}
-  "coq-mathcomp-ssreflect" {(>= "2.0.0")}
+  "coq-mathcomp-ssreflect" {(>= "2.0.0") & (< "2.4~")}
   "coq-deriving" {(>= "0.2.0")}
 ]
 tags: [
diff --git a/released/packages/coq-extructures/coq-extructures.0.5.0/opam b/released/packages/coq-extructures/coq-extructures.0.5.0/opam
index b1ea13bc1ac84e1d35c3a5eba57f412333eb7e3f..4c24a2dd044094ff406bdf764f5667d7cfa5f218 100644
--- a/released/packages/coq-extructures/coq-extructures.0.5.0/opam
+++ b/released/packages/coq-extructures/coq-extructures.0.5.0/opam
@@ -14,7 +14,7 @@ install: [
 ]
 depends: [
   "coq" {(>= "8.17" & < "9.1~")}
-  "coq-mathcomp-ssreflect" {(>= "2.0.0")}
+  "coq-mathcomp-ssreflect" {(>= "2.0.0") & (< "2.4~")}
   "coq-deriving" {(>= "0.2.0")}
 ]
 tags: [
diff --git a/released/packages/coq-graph-theory-planar/coq-graph-theory-planar.0.9.6/opam b/released/packages/coq-graph-theory-planar/coq-graph-theory-planar.0.9.6/opam
new file mode 100644
index 0000000000000000000000000000000000000000..4f28befea80ecd6f84a9d72cbcb481c8a5f4f510
--- /dev/null
+++ b/released/packages/coq-graph-theory-planar/coq-graph-theory-planar.0.9.6/opam
@@ -0,0 +1,39 @@
+opam-version: "2.0"
+maintainer: "christian.doczkal@mpi-sp.org"
+
+homepage: "https://github.com/coq-community/graph-theory"
+dev-repo: "git+https://github.com/coq-community/graph-theory.git"
+bug-reports: "https://github.com/coq-community/graph-theory/issues"
+license: "CECILL-B"
+
+synopsis: "Graph theory results on planarity in Coq and MathComp"
+description: """
+Formal definitions and results on graph planarity in Coq using the Mathematical Components
+library, including Wagner's Theorem. Relies on hypermaps and other notions developed
+as part of the Coq proof of the Four-Color Theorem."""
+
+build: ["dune" "build" "-p" name "-j" jobs]
+depends: [
+  "dune" {>= "3.5"}
+  "coq" {>= "8.18" & < "9.1~"}
+  "coq-mathcomp-ssreflect" {>= "2.1" & < "2.5~"}
+  "coq-graph-theory" {= version}
+  "coq-fourcolor"
+]
+
+tags: [
+  "category:Computer Science/Graph Theory"
+  "keyword:graph theory"
+  "keyword:planarity"
+  "logpath:GraphTheory.planar"
+  "date:2024-06-30"
+]
+authors: [
+  "Christian Doczkal"
+  "Damien Pous"
+]
+
+url {
+  src: "https://github.com/coq-community/graph-theory/releases/download/v0.9.6/graph-theory-0.9.6.tar.gz"
+  checksum: "sha512=61bd37facc9341c45cb8393b6be5885a424208c74c09eb8366fc263bd7f0904bd6b4c5bd419add4fcdc01d244d6a261701ec33469b6e645b54f8a89c95bb5485"
+}
diff --git a/released/packages/coq-graph-theory/coq-graph-theory.0.9.6/opam b/released/packages/coq-graph-theory/coq-graph-theory.0.9.6/opam
new file mode 100644
index 0000000000000000000000000000000000000000..83075acfcadc53e19beb00687c8f086747524f95
--- /dev/null
+++ b/released/packages/coq-graph-theory/coq-graph-theory.0.9.6/opam
@@ -0,0 +1,42 @@
+opam-version: "2.0"
+maintainer: "christian.doczkal@mpi-sp.org"
+
+homepage: "https://github.com/coq-community/graph-theory"
+dev-repo: "git+https://github.com/coq-community/graph-theory.git"
+bug-reports: "https://github.com/coq-community/graph-theory/issues"
+license: "CECILL-B"
+
+synopsis: "General graph theory definitions and results in Coq and MathComp"
+description: """
+Formalized general graph theory definitions and results using Coq and
+the Mathematical Components library, including various standard results
+from the literature (e.g., Menger's Theorem and Hall's Marriage Theorem)."""
+
+build: ["dune" "build" "-p" name "-j" jobs]
+depends: [
+  "dune" {>= "3.5"}
+  "coq" {>= "8.18" & < "9.1~"}
+  "coq-mathcomp-ssreflect" {>= "2.1" & < "2.5~"}
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-finmap"
+  "coq-hierarchy-builder" {>= "1.5.0"}
+]
+
+tags: [
+  "category:Computer Science/Graph Theory"
+  "keyword:graph theory"
+  "keyword:minors"
+  "keyword:treewidth"
+  "keyword:algebra"
+  "logpath:GraphTheory.core"
+  "date:2024-06-30"
+]
+authors: [
+  "Christian Doczkal"
+  "Damien Pous"
+]
+
+url {
+  src: "https://github.com/coq-community/graph-theory/releases/download/v0.9.6/graph-theory-0.9.6.tar.gz"
+  checksum: "sha512=61bd37facc9341c45cb8393b6be5885a424208c74c09eb8366fc263bd7f0904bd6b4c5bd419add4fcdc01d244d6a261701ec33469b6e645b54f8a89c95bb5485"
+}
diff --git a/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.4.0/opam b/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.4.0/opam
new file mode 100644
index 0000000000000000000000000000000000000000..96cf9547644e688c7cb5e0572f6423bcd9277cd8
--- /dev/null
+++ b/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.4.0/opam
@@ -0,0 +1,29 @@
+opam-version: "2.0"
+maintainer: "pierre-yves@strub.nu"
+homepage: "https://github.com/math-comp/multinomials"
+bug-reports: "https://github.com/math-comp/multinomials/issues"
+dev-repo: "git+https://github.com/math-comp/multinomials.git"
+license: "CECILL-B"
+authors: ["Pierre-Yves Strub"]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+   ("coq" {>= "8.18" & < "8.21~"}
+   | "coq-core" {>= "9.0" & < "9.1~"})
+  "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.5~") | = "dev"}
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-bigenough" {(>= "1.0" & < "1.1~") | = "dev"}
+  "coq-mathcomp-finmap"    {(>= "2.0" & < "2.3~") | = "dev"}
+]
+tags: [
+  "keyword:multinomials"
+  "keyword:monoid algebra"
+  "category:Mathematics/Algebra/Multinomials"
+  "category:Mathematics/Algebra/Monoid algebra"
+  "logpath:mathcomp.multinomials"
+]
+synopsis: "A Multivariate polynomial Library for the Mathematical Components Library"
+url {
+  src: "https://github.com/math-comp/multinomials/archive/2.4.0.tar.gz"
+  checksum: "sha512=9ef2deee0542de6a80cbd3785333bc8eb0e65440622e0f7582b35bb69ef382de83ee78a8baacd7074859be92cb15a26fbce8ab33d454e9c158dbbc9f5a17a091"
+}
diff --git a/released/packages/coq-mathcomp-odd-order/coq-mathcomp-odd-order.2.2.0/opam b/released/packages/coq-mathcomp-odd-order/coq-mathcomp-odd-order.2.2.0/opam
new file mode 100644
index 0000000000000000000000000000000000000000..bdb091da2e56a814608d0099422bfbbd01b06789
--- /dev/null
+++ b/released/packages/coq-mathcomp-odd-order/coq-mathcomp-odd-order.2.2.0/opam
@@ -0,0 +1,39 @@
+opam-version: "2.0"
+maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+homepage: "https://math-comp.github.io/math-comp/"
+bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+dev-repo: "git+https://github.com/math-comp/odd-order"
+license: "CeCILL-B"
+
+build: [
+  [make "-j" "%{jobs}%"]
+]
+install: [ make "install" ]
+depends: [
+  "coq-mathcomp-character" {>= "2.2.0" & < "2.5~"}
+]
+tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
+authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
+synopsis: "The formal proof of the Feit-Thompson theorem"
+description: """
+The formal proof of the Feit-Thompson theorem.
+
+From mathcomp Require Import all_ssreflect all_fingroup all_solvable PFsection14.
+
+Check Feit_Thompson.
+   : forall (gT : finGroupType) (G : {group gT}), odd #|G| -> solvable G
+
+From mathcomp Require Import all_ssreflect all_fingroup 
+                             all_solvable stripped_odd_order_theorem.
+
+Check stripped_Odd_Order.
+   : forall (T : Type) (mul : T -> T -> T) (one : T) (inv : T -> T)
+         (G : T -> Type) (n : natural),
+       group_axioms T mul one inv ->
+       group T mul one inv G ->
+       finite_of_order T G n -> odd n -> solvable_group T mul one inv G"""
+
+url {
+  src: "https://github.com/math-comp/odd-order/archive/mathcomp-odd-order.2.2.0.tar.gz"
+  checksum: "sha256=d74c7ef067114b8678dd17d640dc2ee96eb95ba346b6007929919809c87ce7a1"
+}
diff --git a/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.3/opam b/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.3/opam
new file mode 100644
index 0000000000000000000000000000000000000000..3efe97360f275c93b403cde2b40f7dfe00c798c5
--- /dev/null
+++ b/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.3/opam
@@ -0,0 +1,42 @@
+opam-version: "2.0"
+maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
+
+homepage: "https://github.com/math-comp/real-closed"
+dev-repo: "git+https://github.com/math-comp/real-closed.git"
+bug-reports: "https://github.com/math-comp/real-closed/issues"
+license: "CECILL-B"
+
+synopsis: "Mathematical Components Library on real closed fields"
+description: """
+This library contains definitions and theorems about real closed
+fields, with a construction of the real closure and the algebraic
+closure (including a proof of the fundamental theorem of
+algebra). It also contains a proof of decidability of the first
+order theory of real closed field, through quantifier elimination."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+   ("coq" {>= "8.18" & < "8.21~"}
+   | "coq-core" {>= "9.0" & < "9.1~"})
+  "coq" {>= "8.18" & < "9.1~"}
+  "coq-mathcomp-ssreflect" {>= "2.2.0" & < "2.5~"}
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-field"
+  "coq-mathcomp-bigenough" {>= "1.0.0"}
+]
+
+tags: [
+  "keyword:real closed field"
+  "logpath:mathcomp.real_closed"
+  "date:2024-12-09"
+]
+authors: [
+  "Cyril Cohen"
+  "Assia Mahboubi"
+]
+
+url {
+  src: "https://github.com/math-comp/real-closed/archive/2.0.3.tar.gz"
+  checksum: "sha256=d8399b22da69ceda55db12b420b24066871f453ae37e9b206e94c95e5d3761d5"
+}
diff --git a/released/packages/coq-mathcomp-tarjan/coq-mathcomp-tarjan.1.0.2/opam b/released/packages/coq-mathcomp-tarjan/coq-mathcomp-tarjan.1.0.2/opam
index dbd6205712c0f81e2ed3e6a46d1d7e0b093fea8a..003df982e1705c7ed145070d8c4b18d028fb8288 100644
--- a/released/packages/coq-mathcomp-tarjan/coq-mathcomp-tarjan.1.0.2/opam
+++ b/released/packages/coq-mathcomp-tarjan/coq-mathcomp-tarjan.1.0.2/opam
@@ -17,7 +17,7 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" {>= "8.16" & < "9.1~"}
-  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-mathcomp-ssreflect" {>= "2.0" & < "2.4~"}
   "coq-mathcomp-fingroup"
   "coq-hierarchy-builder" {>= "1.4.0"}
 ]
diff --git a/released/packages/coq-mathcomp-tarjan/coq-mathcomp-tarjan.1.0.3/opam b/released/packages/coq-mathcomp-tarjan/coq-mathcomp-tarjan.1.0.3/opam
new file mode 100644
index 0000000000000000000000000000000000000000..50a889c0f5ac3bc9be784272e723bdeb81ce378e
--- /dev/null
+++ b/released/packages/coq-mathcomp-tarjan/coq-mathcomp-tarjan.1.0.3/opam
@@ -0,0 +1,46 @@
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/tarjan"
+dev-repo: "git+https://github.com/coq-community/tarjan.git"
+bug-reports: "https://github.com/coq-community/tarjan/issues"
+license: "CECILL-B"
+
+synopsis: "Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp"
+description: """
+This development contains formalizations and correctness proofs, using Coq and the Mathematical
+Components library, of algorithms originally due to Kosaraju and Tarjan for finding strongly
+connected components in finite graphs. It also contains a verified implementation of topological
+sorting with extended guarantees for acyclic graphs."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.16" & < "9.1~"}
+  "coq-mathcomp-ssreflect" {>= "2.0" & < "2.5~"}
+  "coq-mathcomp-fingroup"
+  "coq-hierarchy-builder" {>= "1.4.0"}
+]
+
+tags: [
+  "category:Computer Science/Graph Theory"
+  "keyword:strongly connected components"
+  "keyword:topological sorting"
+  "keyword:Kosaraju"
+  "keyword:Tarjan"
+  "keyword:acyclicity"
+  "keyword:graph theory"
+  "logpath:mathcomp.tarjan"
+  "date:2023-08-06"
+]
+authors: [
+  "Cyril Cohen"
+  "Jean-Jacques Lévy"
+  "Karl Palmskog"
+  "Laurent Théry"
+]
+
+url {
+  src: "https://github.com/coq-community/tarjan/archive/1.0.3.tar.gz"
+  checksum: "sha256=6f24af7801e560c819c48e562785b3145ef33666458cd8e014761e96b8bfced9"
+}
diff --git a/released/packages/coq-reglang/coq-reglang.1.2.2/opam b/released/packages/coq-reglang/coq-reglang.1.2.2/opam
new file mode 100644
index 0000000000000000000000000000000000000000..c08e1271a65b0318da553d6c379f9bb1ae65518d
--- /dev/null
+++ b/released/packages/coq-reglang/coq-reglang.1.2.2/opam
@@ -0,0 +1,45 @@
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/reglang"
+dev-repo: "git+https://github.com/coq-community/reglang.git"
+bug-reports: "https://github.com/coq-community/reglang/issues"
+doc: "https://coq-community.github.io/reglang/"
+license: "CECILL-B"
+
+synopsis: "Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp"
+description: """
+This library provides definitions and verified translations between
+different representations of regular languages: various forms of
+automata (deterministic, nondeterministic, one-way, two-way),
+regular expressions, and the logic WS1S. It also contains various
+decidability results and closure properties of regular languages."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.16" & < "9.1~"}
+  "coq-mathcomp-ssreflect" {>= "2.0" & < "2.5"}
+  "coq-hierarchy-builder" {>= "1.4.0"}
+]
+
+tags: [
+  "category:Computer Science/Formal Languages Theory and Automata"
+  "keyword:regular languages"
+  "keyword:regular expressions"
+  "keyword:finite automata"
+  "keyword:two-way automata"
+  "keyword:monadic second-order logic"
+  "logpath:RegLang"
+  "date:2024-01-19"
+]
+authors: [
+  "Christian Doczkal"
+  "Jan-Oliver Kaiser"
+  "Gert Smolka"
+]
+
+url {
+  src: "https://github.com/coq-community/reglang/releases/download/v1.2.2/reglang-1.2.2.tar.gz"
+  checksum: "sha512=d30ceffa9e087b8bf84a578a3b85732a1ac84d70b316b3f9666b6ef93b4884d020d5a2efba054295cf47e8c3da3249bd07d5721c82f809a96ad75bcc1804a756"
+}