diff --git a/released/packages/coq-hol-light-real/coq-hol-light-real.1.0.0/opam b/released/packages/coq-hol-light-real/coq-hol-light-real.1.0.0/opam
index 1a7712549..5acc4bfbc 100644
--- a/released/packages/coq-hol-light-real/coq-hol-light-real.1.0.0/opam
+++ b/released/packages/coq-hol-light-real/coq-hol-light-real.1.0.0/opam
@@ -11,7 +11,11 @@ doc: "https://github.com/Deducteam/coq-hol-light-real"
 maintainer: "frederic.blanqui@inria.fr"
 authors: ["Frédéric Blanqui"]
 license: "CeCILL-2.1"
-depends: [ "coq" {>= "8.19"} ]
+depends: [
+  "coq" {>= "8.19"}
+  "coq-mathcomp-ssreflect" {>= "2.1.0"}
+  "coq-mathcomp-algebra" {>= "2.1.0"}
+]
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 tags: [