diff --git a/rocq-mathcomp-analysis.opam b/rocq-mathcomp-analysis.opam
index 3e06f39691..4f9a342048 100644
--- a/rocq-mathcomp-analysis.opam
+++ b/rocq-mathcomp-analysis.opam
@@ -19,7 +19,7 @@ depends: [
   "rocq-mathcomp-solvable"
   "rocq-mathcomp-field"
   "rocq-mathcomp-bigenough" { (>= "1.0.0") }
-  "rocq-navi" {= "0.4.1" & with-doc}
+  "rocq-navi" {= "0.5.1" & with-doc}
 ]
 
 conflicts: [ "coq-mathcomp-analysis" { < "1.16~" } ]