diff --git a/coq-mathcomp-multinomials.opam b/coq-mathcomp-multinomials.opam
index 1825ed8..1d63640 100644
--- a/coq-mathcomp-multinomials.opam
+++ b/coq-mathcomp-multinomials.opam
@@ -8,7 +8,7 @@ license: "CeCILL-B"
 authors: ["Pierre-Yves Strub"]
 build: [ "dune" "build" "-p" name "-j" jobs ]
 depends: [
-  "coq"                    {>= "8.10" & < "8.13~"}
+  "coq"                    {>= "8.10" & < "8.14~"}
   "dune"                   {>= "2.5"}
   "coq-mathcomp-ssreflect" {>= "1.12" & < "1.13~"}
   "coq-mathcomp-algebra"
diff --git a/src/mpoly.v b/src/mpoly.v
index 5787648..0b8aab5 100644
--- a/src/mpoly.v
+++ b/src/mpoly.v
@@ -5313,7 +5313,7 @@ case: (mdeg m =P d)=> /eqP; rewrite basis_cover -/b.
   rewrite mcoeffZ mcoeffX eqxx mulr1 big1 ?addr0 // => m' ne.
   by rewrite mcoeffZ mcoeffX (negbTE ne) mulr0.
 move=> m_notin_b; rewrite big_seq big1 /=.
-  apply/esym/(dhomog_nemf_coeff (mf0 := [measure of mdeg]) (d := d)).
+  apply/esym/(@dhomog_nemf_coeff _ _ [measure of mdeg] d).
     by apply/dhomog_is_dhomog. by rewrite basis_cover.
 move=> m'; apply/contraTeq; rewrite mcoeffZ mcoeffX.
 by case: (m' =P m)=> [->|_]; last rewrite mulr0 eqxx.