diff --git a/released/packages/coq-bedrock2-compiler/coq-bedrock2-compiler.0.0.6/opam b/released/packages/coq-bedrock2-compiler/coq-bedrock2-compiler.0.0.6/opam
index 6f5eba74bb..ebb2cb3b41 100644
--- a/released/packages/coq-bedrock2-compiler/coq-bedrock2-compiler.0.0.6/opam
+++ b/released/packages/coq-bedrock2-compiler/coq-bedrock2-compiler.0.0.6/opam
@@ -15,7 +15,7 @@ build: [
 install: [make "EXTERNAL_DEPENDENCIES=1" "install_compiler"]
 depends: [
   "conf-findutils" {build}
-  "coq" {>= "8.15~"}
+  "coq" {>= "8.16~"}
   "coq-bedrock2" {= "0.0.6"}
   "coq-riscv" {= "0.0.4"}
   "zarith" {>= "1.11"}
diff --git a/released/packages/coq-bedrock2/coq-bedrock2.0.0.6/opam b/released/packages/coq-bedrock2/coq-bedrock2.0.0.6/opam
index a0b67c0b6a..774aa10b0b 100644
--- a/released/packages/coq-bedrock2/coq-bedrock2.0.0.6/opam
+++ b/released/packages/coq-bedrock2/coq-bedrock2.0.0.6/opam
@@ -18,8 +18,8 @@ run-test: [
 depends: [
   "conf-findutils" {build}
   "conf-python-3" {build & with-test}
-  "coq" {>= "8.15~"}
-  "coq-coqutil" {= "0.0.3"}
+  "coq" {>= "8.16~"}
+  "coq-coqutil" {= "0.0.4"}
   "zarith" {>= "1.11"}
 ]
 dev-repo: "git+https://github.com/mit-plv/bedrock2.git"
diff --git a/released/packages/coq-fiat-crypto/coq-fiat-crypto.0.0.20/opam b/released/packages/coq-fiat-crypto/coq-fiat-crypto.0.0.20/opam
index 35a265fe2e..d61ecbb792 100644
--- a/released/packages/coq-fiat-crypto/coq-fiat-crypto.0.0.20/opam
+++ b/released/packages/coq-fiat-crypto/coq-fiat-crypto.0.0.20/opam
@@ -20,7 +20,7 @@ depends: [
   "ocamlfind" {build}
   "coq" {>= "8.15~"}
   "coq-coqprime" {>= "1.2.0"}
-  "coq-rewriter" {>= "0.0.6" & <= "0.0.8"}
+  "coq-rewriter" {>= "0.0.6" & <= "0.0.9"}
   "coq-rupicola" {= "0.0.7"}
   "coq-bedrock2-compiler" {= "0.0.5"}
 ]
diff --git a/released/packages/coq-fiat-crypto/coq-fiat-crypto.0.0.24/opam b/released/packages/coq-fiat-crypto/coq-fiat-crypto.0.0.24/opam
index 183c22dcf3..3d5109a35d 100644
--- a/released/packages/coq-fiat-crypto/coq-fiat-crypto.0.0.24/opam
+++ b/released/packages/coq-fiat-crypto/coq-fiat-crypto.0.0.24/opam
@@ -18,11 +18,11 @@ depends: [
   "conf-findutils" {build}
   "ocaml" {build & >= "4.08~"}
   "ocamlfind" {build}
-  "coq" {>= "8.15~"}
+  "coq" {>= "8.16~"}
   "coq-coqprime" {>= "1.2.0"}
-  "coq-rewriter" {>= "0.0.6" & <= "0.0.8"}
-  "coq-rupicola" {= "0.0.7"}
-  "coq-bedrock2-compiler" {= "0.0.5"}
+  "coq-rewriter" {>= "0.0.6" & <= "0.0.9"}
+  "coq-rupicola" {= "0.0.8"}
+  "coq-bedrock2-compiler" {= "0.0.6"}
 ]
 conflict-class: [
   "coq-fiat-crypto"
diff --git a/released/packages/coq-riscv/coq-riscv.0.0.4/opam b/released/packages/coq-riscv/coq-riscv.0.0.4/opam
index 958e530c56..a84e342ecb 100644
--- a/released/packages/coq-riscv/coq-riscv.0.0.4/opam
+++ b/released/packages/coq-riscv/coq-riscv.0.0.4/opam
@@ -12,7 +12,7 @@ build: [
 install: [make "EXTERNAL_DEPENDENCIES=1" "install"]
 depends: [
   "coq" {>= "8.15~"}
-  "coq-coqutil" {= "0.0.3"}
+  "coq-coqutil" {>= "0.0.3" & <= "0.0.4"}
   "coq-record-update" {>= "0.3.0"}
 ]
 dev-repo: "git+https://github.com/mit-plv/riscv-coq.git"
diff --git a/released/packages/coq-rupicola/coq-rupicola.0.0.8/opam b/released/packages/coq-rupicola/coq-rupicola.0.0.8/opam
index bc195b4407..5e2fc5a053 100644
--- a/released/packages/coq-rupicola/coq-rupicola.0.0.8/opam
+++ b/released/packages/coq-rupicola/coq-rupicola.0.0.8/opam
@@ -16,8 +16,8 @@ build: [
 install: [make "EXTERNAL_DEPENDENCIES=1" "install"]
 depends: [
   "conf-findutils" {build}
-  "coq" {>= "8.15~"}
-  "coq-bedrock2" {= "0.0.5"}
+  "coq" {>= "8.16~"}
+  "coq-bedrock2" {= "0.0.6"}
 ]
 dev-repo: "git+https://github.com/mit-plv/rupicola.git"
 synopsis: "Gallina to imperative code compilation, currently in design phase"