diff --git a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam
index 3931b38c7..b547e24cf 100644
--- a/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam
+++ b/released/packages/coq-fcsl-pcm/coq-fcsl-pcm.2.1.0/opam
@@ -21,7 +21,7 @@ This library relies on propositional and functional extentionality axioms."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq" {>= "8.19" & < "9.1~"}
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-hierarchy-builder" { (>= "1.7.0" & < "1.9~") | (= "dev") }
   "coq-mathcomp-algebra" 
diff --git a/released/packages/coq-htt/coq-htt.2.1.0/opam b/released/packages/coq-htt/coq-htt.2.1.0/opam
index 2bb496d77..e963c2079 100644
--- a/released/packages/coq-htt/coq-htt.2.1.0/opam
+++ b/released/packages/coq-htt/coq-htt.2.1.0/opam
@@ -30,7 +30,7 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: [make "-C" "examples" "-j%{jobs}%"]
 install: [make "-C" "examples" "install"]
 depends: [
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq" {>= "8.19" & < "9.1~"}
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup"