diff --git a/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam b/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam
index f6a8295c7..e7bcd24e8 100644
--- a/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam
+++ b/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam
@@ -9,18 +9,16 @@ license: "CECILL-B"
 synopsis: "Ring, field, lra, nra, and psatz tactics for Mathematical Components"
 description: """
 This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for
-algebraic structures of the Mathematical Components library. The `ring` tactic
-works with any `comRingType` (commutative ring) or `comSemiRingType`
-(commutative semiring). The `field` tactic works with any `fieldType` (field).
-The other (Micromega) tactics work with any `realDomainType` (totally ordered
-integral domain) or `realFieldType` (totally ordered field). Algebra Tactics
-do not provide a way to declare instances, like the `Add Ring` and `Add Field`
-commands, but use canonical structure inference instead. Therefore, each of
-these tactics works with any canonical (or abstract) instance of the
-respective structure declared through Hierarchy Builder. Another key feature
-of Algebra Tactics is that they automatically push down ring morphisms and
-additive functions to leaves of ring/field expressions before applying the
-proof procedures."""
+the Mathematical Components library. These tactics use the algebraic
+structures defined in the MathComp library and their canonical instances for
+the instance resolution, and do not require any special instance declaration,
+like the `add Ring` and `Add Field` commands. Therefore, each of these tactics
+works with any instance of the respective structure, including concrete
+instances declared through Hierarchy Builder, abstract instances, and mixed
+concrete and abstract instances, e.g., `int * R` where `R` is an abstract
+commutative ring. Another key feature of Algebra Tactics is that they
+automatically push down ring morphisms and additive functions to leaves of
+ring/field expressions before applying the proof procedures."""
 
 build: [make "-j%{jobs}%"]
 install: [make "install"]
diff --git a/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.2/opam b/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.2/opam
new file mode 100644
index 000000000..f9847a67c
--- /dev/null
+++ b/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.2/opam
@@ -0,0 +1,43 @@
+opam-version: "2.0"
+maintainer: "kazuhiko.sakaguchi@inria.fr"
+
+homepage: "https://github.com/math-comp/algebra-tactics"
+dev-repo: "git+https://github.com/math-comp/algebra-tactics.git"
+bug-reports: "https://github.com/math-comp/algebra-tactics/issues"
+license: "CECILL-B"
+
+synopsis: "Ring, field, lra, nra, and psatz tactics for Mathematical Components"
+description: """
+This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for
+the Mathematical Components library. These tactics use the algebraic
+structures defined in the MathComp library and their canonical instances for
+the instance resolution, and do not require any special instance declaration,
+like the `add Ring` and `Add Field` commands. Therefore, each of these tactics
+works with any instance of the respective structure, including concrete
+instances declared through Hierarchy Builder, abstract instances, and mixed
+concrete and abstract instances, e.g., `int * R` where `R` is an abstract
+commutative ring. Another key feature of Algebra Tactics is that they
+automatically push down ring morphisms and additive functions to leaves of
+ring/field expressions before applying the proof procedures."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.16" & < "8.19~"}
+  "coq-mathcomp-ssreflect" {>= "2.0" & < "2.1~"}
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-zify" {>= "1.5.0"}
+  "coq-elpi" {>= "1.15.0" & != "1.17.0"}
+]
+
+tags: [
+  "logpath:mathcomp.algebra_tactics"
+]
+authors: [
+  "Kazuhiko Sakaguchi"
+  "Pierre Roux"
+]
+url {
+  src: "https://github.com/math-comp/algebra-tactics/archive/refs/tags/1.2.2.tar.gz"
+  checksum: "sha256=e2c5b2f5ed9dec2db3ac436ebed9e271b2dd760fe5372c57e06fc0619e97a2e4"
+}