Compile with Coq 8.13

erikmd · Jan 8, 2021 · c5b19b6 · c5b19b6
1 parent 4db9d2f
commit c5b19b6
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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.