diff --git a/released/packages/coq-interval/coq-interval.4.6.1/opam b/released/packages/coq-interval/coq-interval.4.6.1/opam
index 080a65a36..d4aefbaea 100644
--- a/released/packages/coq-interval/coq-interval.4.6.1/opam
+++ b/released/packages/coq-interval/coq-interval.4.6.1/opam
@@ -11,7 +11,7 @@ build: [
 ]
 install: ["./remake" "install"]
 depends: [
-  "coq" {>= "8.8.1"}
+  "coq" {>= "8.8.1" & < "8.18~"}
   "coq-bignums" {< "9~"}
   "coq-flocq" {>= "3.1"}
   "coq-mathcomp-ssreflect" {>= "1.6" & < "2~"}
diff --git a/released/packages/coq-interval/coq-interval.4.7.0/opam b/released/packages/coq-interval/coq-interval.4.7.0/opam
index 0460f2829..8ba4cdb82 100644
--- a/released/packages/coq-interval/coq-interval.4.7.0/opam
+++ b/released/packages/coq-interval/coq-interval.4.7.0/opam
@@ -11,7 +11,7 @@ build: [
 ]
 install: ["./remake" "install"]
 depends: [
-  "coq" {>= "8.11"}
+  "coq" {>= "8.11" & < "8.18~"}
   "coq-bignums"
   "coq-flocq" {>= "3.1"}
   "coq-mathcomp-ssreflect" {>= "1.6" & < "2~"}
diff --git a/released/packages/coq-interval/coq-interval.4.8.0/opam b/released/packages/coq-interval/coq-interval.4.8.0/opam
index 913b6db8b..25da7c101 100644
--- a/released/packages/coq-interval/coq-interval.4.8.0/opam
+++ b/released/packages/coq-interval/coq-interval.4.8.0/opam
@@ -11,7 +11,7 @@ build: [
 ]
 install: ["./remake" "install"]
 depends: [
-  "coq" {>= "8.11"}
+  "coq" {>= "8.11" & < "8.18~"}
   "coq-bignums"
   "coq-flocq" {>= "3.1"}
   "coq-mathcomp-ssreflect" {>= "1.6"}
diff --git a/released/packages/coq-interval/coq-interval.4.8.1/opam b/released/packages/coq-interval/coq-interval.4.8.1/opam
new file mode 100644
index 000000000..eeb9c88a9
--- /dev/null
+++ b/released/packages/coq-interval/coq-interval.4.8.1/opam
@@ -0,0 +1,43 @@
+opam-version: "2.0"
+maintainer: "guillaume.melquiond@inria.fr"
+homepage: "https://coqinterval.gitlabpages.inria.fr/"
+dev-repo: "git+https://gitlab.inria.fr/coqinterval/interval.git"
+bug-reports: "https://gitlab.inria.fr/coqinterval/interval/issues"
+license: "CeCILL-C"
+build: [
+  ["autoconf"] {dev}
+  ["./configure"]
+  ["./remake" "-j%{jobs}%"]
+]
+install: ["./remake" "install"]
+depends: [
+  "coq" {>= "8.11"}
+  "coq-bignums"
+  "coq-flocq" {>= "3.1"}
+  "coq-mathcomp-ssreflect" {>= "1.6"}
+  "coq-coquelicot" {>= "3.0"}
+  "conf-autoconf" {build & dev}
+  ("conf-g++" {build} | "conf-clang" {build})
+]
+tags: [
+  "keyword:interval arithmetic"
+  "keyword:decision procedure"
+  "keyword:floating-point arithmetic"
+  "keyword:reflexive tactic"
+  "keyword:Taylor models"
+  "category:Mathematics/Real Calculus and Topology"
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
+  "logpath:Interval"
+  "date:2023-09-08"
+]
+authors: [
+  "Guillaume Melquiond <guillaume.melquiond@inria.fr>"
+  "Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
+  "Pierre Roux <pierre.roux@onera.fr>"
+  "Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>"
+]
+synopsis: "A Coq tactic for proving bounds on real-valued expressions automatically"
+url {
+  src: "https://coqinterval.gitlabpages.inria.fr/releases/interval-4.8.1.tar.gz"
+  checksum: "sha512=d1df6eba5b473f50bf17488d16020b2d377f2c757d58953359d90deb9256fd434a6d4d13ab9c4a075d2dba400e97400064ffe900ca35769df396d53a6d0d53e9"
+}