Adapt to math-comp/math-comp#1031

math-comp · Jun 6, 2023 · 48aef72 · 48aef72
1 parent bc6cbdf
commit 48aef72
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/mpoly.v b/src/mpoly.v
@@ -4662,7 +4662,7 @@ case/tupleP: dt hom => d dt; case/tupleP: mt => p mt /= hom.
 rewrite !big_cons; apply/dhomogM.
   by move: (hom ord0); rewrite (tnth_nth 0) (tnth_nth 0%N).
 apply/ihl => i; have:= hom (inord i.+1).
-by rewrite !(tnth_nth 0) !(tnth_nth 0%N) !inordK ?ltnS.
+by rewrite !(tnth_nth 0) ?(tnth_nth 0%N) !inordK ?ltnS.
 Qed.
 
 End MPolyHomogTheory.