diff --git a/extra-dev/packages/coq-htt-core/coq-htt-core.dev/opam b/extra-dev/packages/coq-htt-core/coq-htt-core.dev/opam
new file mode 100644
index 000000000..390457c71
--- /dev/null
+++ b/extra-dev/packages/coq-htt-core/coq-htt-core.dev/opam
@@ -0,0 +1,58 @@
+opam-version: "2.0"
+maintainer: "fcsl@software.imdea.org"
+
+homepage: "https://github.com/imdea-software/htt"
+dev-repo: "git+https://github.com/imdea-software/htt.git"
+bug-reports: "https://github.com/imdea-software/htt/issues"
+license: "Apache-2.0"
+
+synopsis: "Hoare Type Theory"
+description: """
+Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating
+programs based on Separation logic.
+
+HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A
+Hoare type `ST P (fun x : A => Q)` denotes computations with a precondition `P` and postcondition
+`Q`, returning a value `x` of type `A`. Hoare types are a dependently typed version of monads,
+as used in the programming language Haskell. Monads hygienically combine the language features
+for pure functional programming, with those for imperative programming, such as state or
+exceptions. In this sense, HTT establishes a formal connection in the style of Curry-Howard
+isomorphism between monads and (functional programming variant of) Separation logic. Every
+effectful command in HTT has a type that corresponds to the appropriate non-structural inference
+rule in Separation logic, and vice versa, every non-structural inference rule corresponds to a
+command in HTT that has that rule as the type. The type for monadic bind is the Hoare rule for
+sequential composition, and the type for monadic unit combines the Hoare rules for the idle
+program (in a small-footprint variant) and for variable assignment (adapted for functional
+variables). The connection reconciles dependent types with effects of state and exceptions and
+establishes Separation logic as a type theory for such effects. In implementation terms, it means
+that HTT implements Separation logic as a shallow embedding in Coq."""
+
+build: [make "-C" "htt" "-j%{jobs}%"]
+install: [make "-C" "htt" "install"]
+depends: [
+  "coq" {>= "8.19"}
+  "coq-mathcomp-ssreflect" {>= "2.2.0"}
+  "coq-hierarchy-builder" {>= "1.7.0"}
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-fingroup" 
+  "coq-fcsl-pcm" {>= "2.1.0"}
+]
+
+tags: [
+  "category:Computer Science/Data Types and Data Structures"
+  "keyword:partial commutative monoids"
+  "keyword:separation logic"
+  "logpath:htt"
+]
+
+authors: [
+  "Aleksandar Nanevski"
+  "Germán Andrés Delbianco"
+  "Alexander Gryzlov"
+  "Marcos Grandury"
+]
+
+url {
+  src: "git+https://github.com/imdea-software/htt.git#master"
+}
+
diff --git a/extra-dev/packages/coq-htt/coq-htt.dev/opam b/extra-dev/packages/coq-htt/coq-htt.dev/opam
new file mode 100644
index 000000000..47609191f
--- /dev/null
+++ b/extra-dev/packages/coq-htt/coq-htt.dev/opam
@@ -0,0 +1,59 @@
+opam-version: "2.0"
+maintainer: "fcsl@software.imdea.org"
+
+homepage: "https://github.com/imdea-software/htt"
+dev-repo: "git+https://github.com/imdea-software/htt.git"
+bug-reports: "https://github.com/imdea-software/htt/issues"
+license: "Apache-2.0"
+
+synopsis: "Hoare Type Theory"
+description: """
+Hoare Type Theory (HTT) is a verification system for reasoning about sequential heap-manipulating
+programs based on Separation logic.
+
+HTT incorporates Hoare-style specifications via preconditions and postconditions into types. A
+Hoare type `ST P (fun x : A => Q)` denotes computations with a precondition `P` and postcondition
+`Q`, returning a value `x` of type `A`. Hoare types are a dependently typed version of monads,
+as used in the programming language Haskell. Monads hygienically combine the language features
+for pure functional programming, with those for imperative programming, such as state or
+exceptions. In this sense, HTT establishes a formal connection in the style of Curry-Howard
+isomorphism between monads and (functional programming variant of) Separation logic. Every
+effectful command in HTT has a type that corresponds to the appropriate non-structural inference
+rule in Separation logic, and vice versa, every non-structural inference rule corresponds to a
+command in HTT that has that rule as the type. The type for monadic bind is the Hoare rule for
+sequential composition, and the type for monadic unit combines the Hoare rules for the idle
+program (in a small-footprint variant) and for variable assignment (adapted for functional
+variables). The connection reconciles dependent types with effects of state and exceptions and
+establishes Separation logic as a type theory for such effects. In implementation terms, it means
+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"}
+  "coq-mathcomp-ssreflect" {>= "2.2.0"}
+  "coq-hierarchy-builder" {>= "1.7.0"}
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-fingroup" 
+  "coq-fcsl-pcm" {>= "2.1.0"}
+  "coq-htt-core" {= version}
+]
+
+tags: [
+  "category:Computer Science/Data Types and Data Structures"
+  "keyword:partial commutative monoids"
+  "keyword:separation logic"
+  "logpath:htt"
+]
+
+authors: [
+  "Aleksandar Nanevski"
+  "Germán Andrés Delbianco"
+  "Alexander Gryzlov"
+  "Marcos Grandury"
+]
+
+url {
+  src: "git+https://github.com/imdea-software/htt.git#master"
+}
+
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 f742edec8..1fef6d74b 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,9 +21,9 @@ This library relies on propositional and functional extentionality axioms."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
-  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.9~") | (= "dev") }
+  "coq" {>= "8.19" & < "9.1~"}
+  "coq-mathcomp-ssreflect" {>= "2.2.0" & < "2.4~"}
+  "coq-hierarchy-builder" {>= "1.7.0" & < "1.9~"}
   "coq-mathcomp-algebra" 
 ]
 
diff --git a/released/packages/coq-htt-core/coq-htt-core.2.1.0/opam b/released/packages/coq-htt-core/coq-htt-core.2.1.0/opam
index 5cd0bea50..914469fc6 100644
--- a/released/packages/coq-htt-core/coq-htt-core.2.1.0/opam
+++ b/released/packages/coq-htt-core/coq-htt-core.2.1.0/opam
@@ -30,11 +30,11 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: [make "-C" "htt" "-j%{jobs}%"]
 install: [make "-C" "htt" "install"]
 depends: [
-  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
+  "coq" {>= "8.19" & < "9.1~"}
+  "coq-mathcomp-ssreflect" {>= "2.2.0" & < "2.4~"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }
+  "coq-fcsl-pcm" {>= "2.1.0" & < "2.2~"}
 ]
 
 tags: [
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 0d9d98500..3f4eb26da 100644
--- a/released/packages/coq-htt/coq-htt.2.1.0/opam
+++ b/released/packages/coq-htt/coq-htt.2.1.0/opam
@@ -30,11 +30,11 @@ 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" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
+  "coq" {>= "8.19" & < "9.1~"}
+  "coq-mathcomp-ssreflect" {>= "2.2.0" & < "2.4~"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }
+  "coq-fcsl-pcm" {>= "2.1.0" & < "2.2~"}
   "coq-htt-core" {= version}
 ]