diff --git a/released/packages/coq-autosubst/coq-autosubst.1.9/opam b/released/packages/coq-autosubst/coq-autosubst.1.9/opam
index 84c16c5435..6fce2492b8 100644
--- a/released/packages/coq-autosubst/coq-autosubst.1.9/opam
+++ b/released/packages/coq-autosubst/coq-autosubst.1.9/opam
@@ -19,7 +19,7 @@ substitutions."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.14" & < "8.21~"}
+  "coq" {>= "8.14" & < "9.1~"}
 ]
 
 tags: [
diff --git a/released/packages/coq-color/coq-color.1.8.5/opam b/released/packages/coq-color/coq-color.1.8.5/opam
index 0fa73a1cca..6eb0e215bd 100644
--- a/released/packages/coq-color/coq-color.1.8.5/opam
+++ b/released/packages/coq-color/coq-color.1.8.5/opam
@@ -24,7 +24,7 @@ install: [make "-f" "Makefile.coq" "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/CoLoR"]
 depends: [
   "ocaml"
-  "coq" {>= "8.14" & < "8.21~"}
+  "coq" {>= "8.14" & < "9.1~"}
   "coq-bignums"
 ]
 tags: [
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 21b365d0d7..5ea486a2aa 100644
--- a/released/packages/coq-deriving/coq-deriving.0.2.1/opam
+++ b/released/packages/coq-deriving/coq-deriving.0.2.1/opam
@@ -9,7 +9,7 @@ license: "MIT"
 build: [ make "-j" "%{jobs}%" "test" {with-test} ]
 install: [ make "install" ]
 depends: [
-  "coq" { (>= "8.17" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.17" & < "9.1~") | (= "dev") }
   "coq-mathcomp-ssreflect" {>= "2.0"}
 ]
 
diff --git a/released/packages/coq-elpi/coq-elpi.2.4.0/opam b/released/packages/coq-elpi/coq-elpi.2.4.0/opam
index 2394a283cf..16dacff077 100644
--- a/released/packages/coq-elpi/coq-elpi.2.4.0/opam
+++ b/released/packages/coq-elpi/coq-elpi.2.4.0/opam
@@ -18,7 +18,7 @@ depends: [
   "dune" {>= "3.13"}
   "ocaml" {>= "4.10.0"}
   "elpi" {>= "2.0.7" & < "2.1.0~"}
-  "coq" {>= "8.20+rc1" & < "8.21~"}
+  "coq" {>= "8.20+rc1" & < "9.1~"}
   "ppx_optcomp"
   "ocaml-lsp-server" {with-dev-setup}
   "odoc" {with-doc}
@@ -45,4 +45,4 @@ url {
   checksum: [
     "sha512=327cf88912571884f5d5598c658b47c73694cf8fbc74cf7a2c65eb2577c3adc6b767c49c18216e19cf59c1661e315265e82e9b7a2226305ae56bee6bc9895b9d"
   ]
-}
\ No newline at end of file
+}
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 8741647bcb..b1ea13bc1a 100644
--- a/released/packages/coq-extructures/coq-extructures.0.5.0/opam
+++ b/released/packages/coq-extructures/coq-extructures.0.5.0/opam
@@ -13,7 +13,7 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {(>= "8.17" & < "8.21~")}
+  "coq" {(>= "8.17" & < "9.1~")}
   "coq-mathcomp-ssreflect" {(>= "2.0.0")}
   "coq-deriving" {(>= "0.2.0")}
 ]
diff --git a/released/packages/coq-fourcolor/coq-fourcolor.1.4.0/opam b/released/packages/coq-fourcolor/coq-fourcolor.1.4.0/opam
index 9e46cf1215..7fee942463 100644
--- a/released/packages/coq-fourcolor/coq-fourcolor.1.4.0/opam
+++ b/released/packages/coq-fourcolor/coq-fourcolor.1.4.0/opam
@@ -16,9 +16,9 @@ basic plane topology definitions, and a theory of combinatorial hypermaps."""
 build: [make "-C" "theories/proof" "-j%{jobs}%"]
 install: [make "-C" "theories/proof" "install"]
 depends: [
-  "coq" {(>= "8.16" & < "8.21~") | (= "dev")}
+  "coq" {(>= "8.16" & < "9.1~") | (= "dev")}
   "coq-mathcomp-ssreflect" {(>= "2.1.0" & < "2.4~") | (= "dev")}
-  "coq-mathcomp-algebra" 
+  "coq-mathcomp-algebra"
   "coq-hierarchy-builder" {>= "1.5.0"}
   "coq-fourcolor-reals" {= version}
 ]
diff --git a/released/packages/coq-hierarchy-builder/coq-hierarchy-builder.1.8.1/opam b/released/packages/coq-hierarchy-builder/coq-hierarchy-builder.1.8.1/opam
new file mode 100644
index 0000000000..ad15268d07
--- /dev/null
+++ b/released/packages/coq-hierarchy-builder/coq-hierarchy-builder.1.8.1/opam
@@ -0,0 +1,33 @@
+opam-version: "2.0"
+synopsis:
+  "High level commands to declare and evolve a hierarchy based on packed classes"
+description: """\
+Hierarchy Builder is a high level language to build hierarchies of algebraic structures and make these
+hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder
+and abbreviation that let the hierarchy developer describe an actual interface for their library.
+Behind that interface the developer can provide appropriate code to ensure retro compatibility."""
+maintainer: "Enrico Tassi <enrico.tassi@inria.fr>"
+authors: ["Cyril Cohen" "Kazuhiko Sakaguchi" "Enrico Tassi"]
+license: "MIT"
+tags: "logpath:HB"
+homepage: "https://github.com/math-comp/hierarchy-builder"
+bug-reports: "https://github.com/math-comp/hierarchy-builder/issues"
+depends: [
+  ("coq" {>= "8.18" & < "8.20~"} & "coq-elpi" {>= "2.0"}
+  | "coq" {>= "8.20" | = "dev"} & "coq-elpi" {(>= "2.4" < "2.5") | = "dev"})
+]
+conflicts: ["coq-hierarchy-builder-shim"]
+build: [
+  [make "build"]
+  [make "test-suite"] {with-test}
+]
+install: [make "install"]
+dev-repo: "git+https://github.com/math-comp/hierarchy-builder"
+url {
+  src:
+    "https://github.com/math-comp/hierarchy-builder/releases/download/v1.8.0/hierarchy-builder-1.8.0.tar.gz"
+  checksum: [
+    "md5=faa5a113d28f52b680b7f7b44a090fb9"
+    "sha512=244dab5c4a8f62f4c2fd506ebe7822d68405d1a2c1bae35664028f27ca7776b60bff7446ef232b841335357a24c4d502815c01e8d11ced3318f0d271990f77e6"
+  ]
+}
diff --git a/released/packages/coq-iris/coq-iris.4.3.0/opam b/released/packages/coq-iris/coq-iris.4.3.0/opam
index 12a7916514..e869bacf95 100644
--- a/released/packages/coq-iris/coq-iris.4.3.0/opam
+++ b/released/packages/coq-iris/coq-iris.4.3.0/opam
@@ -27,7 +27,7 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
   "coq-stdpp" { (= "1.11.0") | (= "dev") }
 ]
 
diff --git a/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.4/opam b/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.4/opam
new file mode 100644
index 0000000000..2074afb1b9
--- /dev/null
+++ b/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.4/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" & < "9.1~"}
+  "coq-mathcomp-ssreflect" {>= "2.0" & < "2.4~"}
+  "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.3.tar.gz"
+  checksum: "sha256=a556875e9ed8db1f77474de77c6ae56142c4477a9f11438d70e1f346c90001e4"
+}
diff --git a/released/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.2/opam b/released/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.2/opam
new file mode 100644
index 0000000000..2593176dd1
--- /dev/null
+++ b/released/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.2/opam
@@ -0,0 +1,39 @@
+
+opam-version: "2.0"
+maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
+
+homepage: "https://github.com/math-comp/bigenough"
+dev-repo: "git+https://github.com/math-comp/bigenough.git"
+bug-reports: "https://github.com/math-comp/bigenough/issues"
+license: "CeCILL-B"
+
+synopsis: "A small library to do epsilon - N reasoning"
+description: """
+The package contains a package to reasoning with big enough objects
+(mostly natural numbers). This package is essentially for backward
+compatibility purposes as `bigenough` will be subsumed by the near
+tactics. The formalization is based on the Mathematical Components
+library."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {(>= "8.10" & < "9.1~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {>= "1.6"}
+]
+
+tags: [
+  "keyword:bigenough"
+  "keyword:asymptotic reasonning"
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "logpath:mathcomp.bigenough"
+]
+authors: [
+  "Cyril Cohen"
+]
+
+url {
+  src: "https://github.com/math-comp/bigenough/archive/1.0.2.tar.gz"
+  checksum: "sha512=faaa56c7db5b00a3e3b1a60dc0b3623d8ef5bcf7d08a228df2184e79a124f9dbd4917b2c24cef0bd9ad98b3dd7aae331d5fbe6dd2d154b80fdc108d8dc828b29"
+}
diff --git a/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.8.0/opam b/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.8.0/opam
index 95fe9f4089..9737ad14da 100644
--- a/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.8.0/opam
+++ b/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.8.0/opam
@@ -14,7 +14,7 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.1.0") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
diff --git a/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.2.1.0/opam b/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.2.1.0/opam
index 1bd916e089..9eeab23c60 100644
--- a/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.2.1.0/opam
+++ b/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.2.1.0/opam
@@ -17,7 +17,7 @@ which will be used to subsume notations for finite sets, eventually."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.16" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.16" & < "9.1~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.0.0" & < "2.4~") | (= "dev") }
 ]
 
diff --git a/released/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.1.8.0/opam b/released/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.1.8.0/opam
index 766e9b3535..515c038011 100644
--- a/released/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.1.8.0/opam
+++ b/released/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.1.8.0/opam
@@ -14,6 +14,7 @@ the Coq proof-assistant using the Mathematical Components library and Stdlib."""
 build: [make "-C" "reals_stdlib" "-j%{jobs}%"]
 install: [make "-C" "reals_stdlib" "install"]
 depends: [
+  "coq" {< "8.21~"}
   "coq-mathcomp-reals" { = version}
 ]
 
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
index 472f5d178f..f4a0cc9566 100644
--- 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
@@ -9,7 +9,7 @@ license: "CECILL-B"
 build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
 install: [ make "-C" "mathcomp/ssreflect" "install" ]
 depends: [
-  "coq" {(>= "8.18" & < "8.21~") | (= "dev")}
+  "coq" {(>= "8.18" & < "9.1~") | (= "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"}
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 04ddcd3703..dbd6205712 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
@@ -16,9 +16,9 @@ sorting with extended guarantees for acyclic graphs."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16" & < "8.21~"}
+  "coq" {>= "8.16" & < "9.1~"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
-  "coq-mathcomp-fingroup" 
+  "coq-mathcomp-fingroup"
   "coq-hierarchy-builder" {>= "1.4.0"}
 ]
 
diff --git a/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.5.0+2.0+8.16/opam b/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.5.0+2.0+8.16/opam
index 395b48a34c..9d3c756825 100644
--- a/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.5.0+2.0+8.16/opam
+++ b/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.5.0+2.0+8.16/opam
@@ -15,9 +15,9 @@ by extending the zify tactic."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.16" & < "8.21~")}
+  "coq" {(>= "8.16" & < "9.1~")}
   "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.4~")}
-  "coq-mathcomp-algebra" 
+  "coq-mathcomp-algebra"
 ]
 
 tags: [
diff --git a/released/packages/coq-paco/coq-paco.4.2.2/opam b/released/packages/coq-paco/coq-paco.4.2.2/opam
index 886ea62ccb..6240603c6f 100644
--- a/released/packages/coq-paco/coq-paco.4.2.2/opam
+++ b/released/packages/coq-paco/coq-paco.4.2.2/opam
@@ -15,7 +15,7 @@ license: "BSD-3-Clause"
 build: [make "-C" "src" "all" "-j%{jobs}%"]
 install: [make "-C" "src" "-f" "Makefile.coq" "install"]
 depends: [
-  "coq" {>= "8.13" & < "8.21~"}
+  "coq" {>= "8.13" & < "9.1~"}
 ]
 tags: [
   "date:2024-12-31"
diff --git a/released/packages/coq-record-update/coq-record-update.0.3.4/opam b/released/packages/coq-record-update/coq-record-update.0.3.4/opam
index 33715b66d7..5a3fe508b8 100644
--- a/released/packages/coq-record-update/coq-record-update.0.3.4/opam
+++ b/released/packages/coq-record-update/coq-record-update.0.3.4/opam
@@ -16,7 +16,7 @@ simple typeclass that lists out the record fields."""
 build: [make "-j%{jobs}%" "NO_TEST=1"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.14" & < "8.21~") | (= "dev")}
+  "coq" {(>= "8.14" & < "9.1~") | (= "dev")}
 ]
 
 tags: [
diff --git a/released/packages/coq-reglang/coq-reglang.1.2.1/opam b/released/packages/coq-reglang/coq-reglang.1.2.1/opam
index ca645f2503..6d9399b680 100644
--- a/released/packages/coq-reglang/coq-reglang.1.2.1/opam
+++ b/released/packages/coq-reglang/coq-reglang.1.2.1/opam
@@ -18,7 +18,7 @@ decidability results and closure properties of regular languages."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16" & < "8.21"}
+  "coq" {>= "8.16" & < "9.1~"}
   "coq-mathcomp-ssreflect" {>= "2.0" & < "2.4"}
   "coq-hierarchy-builder" {>= "1.4.0"}
 ]
diff --git a/released/packages/coq-simple-io/coq-simple-io.1.10.0/opam b/released/packages/coq-simple-io/coq-simple-io.1.10.0/opam
index a9f9f54a9c..5d8dfb8ef8 100644
--- a/released/packages/coq-simple-io/coq-simple-io.1.10.0/opam
+++ b/released/packages/coq-simple-io/coq-simple-io.1.10.0/opam
@@ -13,7 +13,7 @@ depends: [
   "dune" {>= "3.7"}
   "ocaml" {>= "4.08.0"}
   "ocamlfind"
-  "coq" {>= "8.12~" & < "8.21~"}
+  "coq" {>= "8.12~" & < "9.1~"}
   "coq-ext-lib" {>= "0.10.0"}
   "ocamlbuild" {with-test & >= "0.9.0"}
   "cppo" {build & >= "1.6.8"}
diff --git a/released/packages/coq-stdpp/coq-stdpp.1.11.0/opam b/released/packages/coq-stdpp/coq-stdpp.1.11.0/opam
index 439db823e9..16fdb5c64c 100644
--- a/released/packages/coq-stdpp/coq-stdpp.1.11.0/opam
+++ b/released/packages/coq-stdpp/coq-stdpp.1.11.0/opam
@@ -33,7 +33,7 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.18" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.18" & < "9.1~") | (= "dev") }
 ]
 
 build: ["./make-package" "stdpp" "-j%{jobs}%"]