diff --git a/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.3.0/opam b/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.3.0/opam
new file mode 100644
index 000000000..6a7ee93c4
--- /dev/null
+++ b/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.3.0/opam
@@ -0,0 +1,64 @@
+opam-version: "2.0"
+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" "mathcomp/algebra" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/algebra" "install" ]
+depends: [ "coq-mathcomp-fingroup" { = version } ]
+
+tags: [
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "keyword:algebra"
+  "keyword:algebraic structure hierarchies"
+  "keyword:archimedean field"
+  "keyword:floor"
+  "keyword:ceil"
+  "keyword:intervals"
+  "keyword:matrices"
+  "keyword:vectors"
+  "keyword:block matrices"
+  "keyword:determinant"
+  "keyword:Cramer rule"
+  "keyword:Vandermonde matrices"
+  "keyword:LUP decomposition"
+  "keyword:Gaussian elimination"
+  "keyword:matrix rank"
+  "keyword:eigen values"
+  "keyword:single variable polynomials"
+  "keyword:bivariate polynomials"
+  "keyword:polynomial division"
+  "keyword:integers"
+  "keyword:rational numbers"
+  "keyword:semirings"
+  "keyword:rings"
+  "keyword:left algebra"
+  "keyword:left module"
+  "keyword:unit rings"
+  "keyword:field"
+  "keyword:algebraically closed field"
+  "keyword:additive morphisms"
+  "keyword:ring morphisms"
+  "keyword:finite dimensional vector spaces"
+  "keyword:complex numbers"
+  "keyword:square root"
+  "logpath:mathcomp.algebra"
+]
+authors: [ "The Mathematical Components team" ]
+
+synopsis: "Mathematical Components Library on Algebra"
+description: """
+This library contains definitions and theorems about discrete
+(i.e. with decidable equality) algebraic structures : ring, fields,
+ordered fields, real fields,  modules, algebras, integers, rational
+numbers, polynomials, matrices, vector spaces...
+"""
+
+url {
+src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz"
+checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec"
+}
diff --git a/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.3.0/opam b/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.3.0/opam
new file mode 100644
index 000000000..4a278df39
--- /dev/null
+++ b/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.3.0/opam
@@ -0,0 +1,31 @@
+opam-version: "2.0"
+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" "mathcomp/character" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/character" "install" ]
+depends: [ "coq-mathcomp-field" { = version } ]
+
+tags: [
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "keyword:algebra"
+  "keyword:character"
+  "logpath:mathcomp.character"
+]
+authors: [ "The Mathematical Components team" ]
+
+synopsis: "Mathematical Components Library on character theory"
+description:"""
+This library contains definitions and theorems about group
+representations, characters and class functions.
+"""
+
+url {
+src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz"
+checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec"
+}
diff --git a/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.3.0/opam b/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.3.0/opam
new file mode 100644
index 000000000..1f0fff5e0
--- /dev/null
+++ b/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.3.0/opam
@@ -0,0 +1,31 @@
+opam-version: "2.0"
+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" "mathcomp/field" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/field" "install" ]
+depends: [ "coq-mathcomp-solvable" { = version } ]
+
+tags: [
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "keyword:algebra"
+  "keyword:field"
+  "logpath:mathcomp.field"
+]
+authors: [ "The Mathematical Components team" ]
+
+synopsis: "Mathematical Components Library on Fields"
+description:"""
+This library contains definitions and theorems about field extensions,
+galois theory, algebraic numbers, cyclotomic polynomials...
+"""
+
+url {
+src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz"
+checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec"
+}
diff --git a/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.3.0/opam b/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.3.0/opam
new file mode 100644
index 000000000..b1146d8d7
--- /dev/null
+++ b/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.3.0/opam
@@ -0,0 +1,30 @@
+opam-version: "2.0"
+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" "mathcomp/fingroup" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/fingroup" "install" ]
+depends: [ "coq-mathcomp-ssreflect" { = version } ]
+
+tags: [
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "keyword:finite groups"
+  "logpath:mathcomp.fingroup"
+]
+authors: [ "The Mathematical Components team" ]
+
+synopsis: "Mathematical Components Library on finite groups"
+description: """
+This library contains definitions and theorems about finite groups,
+group quotients, group morphisms, group presentation, group action...
+"""
+
+url {
+src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz"
+checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec"
+}
diff --git a/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.3.0/opam b/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.3.0/opam
new file mode 100644
index 000000000..82d6c00b8
--- /dev/null
+++ b/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.3.0/opam
@@ -0,0 +1,30 @@
+opam-version: "2.0"
+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" "mathcomp/solvable" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/solvable"  "install" ]
+depends: [ "coq-mathcomp-algebra" { = version } ]
+
+tags: [
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "keyword:finite groups"
+  "logpath:mathcomp.solvable"
+]
+authors: [ "The Mathematical Components team" ]
+
+synopsis: "Mathematical Components Library on finite groups (II)"
+
+description:"""
+This library contains more definitions and theorems about finite groups.
+"""
+
+url {
+src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz"
+checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec"
+}
diff --git a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam
new file mode 100644
index 000000000..472f5d178
--- /dev/null
+++ b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam
@@ -0,0 +1,54 @@
+opam-version: "2.0"
+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" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/ssreflect" "install" ]
+depends: [
+  "coq" {(>= "8.18" & < "8.21~") | (= "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"}
+]
+
+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
+"""
+
+url {
+src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz"
+checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec"
+}