diff --git a/colibrics.opam b/colibrics.opam
index c66fe447a815e9acc520a926c75578ec8e0bdb7f..1d664512898df0a400660ff16928f7de8befa129 100644
--- a/colibrics.opam
+++ b/colibrics.opam
@@ -9,9 +9,9 @@ homepage: "https://colibri.frama-c.com"
 bug-reports: "https://git.frama-c.com/pub/colibrics/issues"
 depends: [
   "ppx_deriving_yojson" {>= "3.6.1"}
-  "dolmen" {>= "0.5~dev"}
-  "dolmen_type" {>= "0.5~dev"}
-  "dolmen_loop" {>= "0.5~dev"}
+  "dolmen" {>= "0.7"}
+  "dolmen_type" {>= "0.7"}
+  "dolmen_loop" {>= "0.7"}
   "dune" {>= "3.0"}
   "zarith" {>= "1.12"}
   "cmdliner" {>= "1.1.1"}
diff --git a/dune-project b/dune-project
index 1b38f375558886a82c0392f04ca8591651397eee..dcac8be62d81a587edaffe265e62bb45c4665ad9 100644
--- a/dune-project
+++ b/dune-project
@@ -19,9 +19,9 @@
   (description "The core of Colibrics is formally proved using Why3.")
   (depends
     ("ppx_deriving_yojson" (>= "3.6.1"))
-    ("dolmen" (>= "0.5~dev"))
-    ("dolmen_type" (>= "0.5~dev"))
-    ("dolmen_loop" (>= "0.5~dev"))
+    ("dolmen" (>= "0.7"))
+    ("dolmen_type" (>= "0.7"))
+    ("dolmen_loop" (>= "0.7"))
     "dune"
     ("zarith" (>= "1.12"))
     ("cmdliner" (>= 1.1.1))