diff --git a/extra-dev/packages/coq-htt/coq-htt.dev/opam b/extra-dev/packages/coq-htt/coq-htt.dev/opam
deleted file mode 100644
index 3a918f739..000000000
--- a/extra-dev/packages/coq-htt/coq-htt.dev/opam
+++ /dev/null
@@ -1,54 +0,0 @@
-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: ["dune" "build" "-p" name "-j" jobs]
-depends: [
-  "dune" {>= "2.5"}
-  "coq" {>= "8.15"}
-  "coq-mathcomp-ssreflect" {>= "1.17.0" & < "2.0"}
-  "coq-mathcomp-algebra"
-  "coq-mathcomp-fingroup"
-  "coq-fcsl-pcm" {>= "1.8.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"
-]
-
-url {
-  src: "git+https://github.com/imdea-software/htt.git#master"
-}