Adapt to math-comp/math-comp#1261

Author: proux01

theories/numbers/ssete8.v

@@ -356,7 +356,7 @@ Lemma shorten_sum (f: nat -> R) (n m : nat):
   \sum_(i < m) f i = \sum_(i < n) f i.
 Proof.
 move => nm fz.
-rewrite - (big_mkord xpredT) (big_cat_nat _ _ _ (leq0n n) nm) /= big_mkord.
+rewrite - (big_mkord xpredT) (@big_cat_nat _ _ _ _ _ _ _ _ (leq0n n) nm) /= big_mkord.  (* FIXME: replace with (big_cat_nat (leq0n n) nm) when requiring MC >= 2.4.0 *)
 rewrite  [X in ( _ + X)]big1_seq ? Monoid.mulm1 // => i; case /andP => _.
 by rewrite mem_index_iota; apply: fz.
 Qed.

theories/stern/fibm.v

@@ -4052,7 +4052,7 @@ Proof.
 move: (fib_ge2_alt n); set p :=  (fib n.+3).-2 => pv.
 have la: (fib n.+2).-1 <= p by rewrite - 2!ltnS -pv -fib_pos fib_smonotone_bis.
 have lb: p <= (fib n.+3).-1 by rewrite pv /=.
-rewrite card_max_repE (big_cat_nat _ _ _ la lb) pv /= big_hasC.
+rewrite card_max_repE (@big_cat_nat _ _ _ _ _ _ _ _ la lb) pv /= big_hasC.  (* FIXME: replace with (big_cat_nat la lb) when requiring MC >= 2.4.0 *)
   by rewrite big_ltn_cond // /p ZeckM_fibm2 size_rev size_iota eqxx big_geq.
 apply/hasPn => i; rewrite mem_index_iota /p.
 case:(posnP n)=> [ | /prednK nv]; first by move ->; rewrite ltn0 andbF.
@@ -4081,7 +4081,7 @@ have kl2: k <= (fib n.+3).-1.
   by rewrite - ltnS /k -addnS -!fib_pos fibSS leq_add2r fib_monotone.
 have np:=(ltn_predK lmn).
 have n3: n = (n-3).+3 by rewrite - addn3 subnK // (leq_trans _ lmn).
-rewrite addnC !card_max_repE (big_cat_nat _ _ _ kl1 kl2) /=; congr addn. 
+rewrite addnC !card_max_repE (@big_cat_nat _ _ _ _ _ _ _ _ kl1 kl2) /=; congr addn.  (* FIXME: replace with (big_cat_nat kl1 kl2) when requiring MC >= 2.4.0 *)
    rewrite fibSS /k -[in fib n] np (fib_pos n.-1) addnS /= np big_nat_shift.
    apply:big_nat_cond_eq => i eq1.
    by rewrite n3 in eq1; move:(ZeckM_rec2 eq1); rewrite -n3 addnC => ->.
@@ -4147,7 +4147,7 @@ case: (posnP n) => np.
 set k := fib n.+2 + fib n.
 have kl1: (fib n.+2) <= k by rewrite leq_addr.
 have kl2: k <= (fib n.+3) by rewrite  fibSS /k leq_add2l fib_monotone.
-rewrite {1} card_min_repE (big_cat_nat _ _ _ kl1 kl2) /=; congr addn. 
+rewrite {1} card_min_repE (@big_cat_nat _ _ _ _ _ _ _ _ kl1 kl2) /=; congr addn.  (* FIXME: replace with (big_cat_nat kl1 kl2) when requiring MC >= 2.4.0 *)
   rewrite /k {1} fibSS !(addnC _ (fib n)) big_nat_shift card_min_repE.
   apply:big_nat_cond_eq => i eq1.
   move/andP:(eq1) => [ha]; rewrite fibSS => hb.

theories/stern/stern.v

@@ -2726,7 +2726,7 @@ rewrite - (big_mkord xpredT (fun i => Stern (i + 2 ^ n.+1).*2)).
 transitivity (p%:Q); last by rewrite expnS ratN_M mulrC mulKf //.
 have ha: (0 <= 2^n)%N by [].
 have hb: (2^n <= 2^n.+1)%N by rewrite leq_exp2l.
-rewrite(big_cat_nat _ _ _ ha hb) /= [X in _ + X] big_nat_rev /=.
+rewrite(@big_cat_nat _ _ _ _ _ _ _ _ ha hb) /= [X in _ + X] big_nat_rev /=.  (* FIXME: replace with (big_cat_nat ha hb) when requiring MC >= 2.4.0 *)
 rewrite -/p -{2} (add0n p) big_addn expn2S -{2} addnn addnK -big_split /=.
 rewrite big_mkord; transitivity (\sum_(i < p) 1 %:Q);
   last by rewrite sumr_const card_ord //.
@@ -4731,7 +4731,7 @@ have: x = #|[set i:'I_m'.+1 | (2^n <= i) && (b == fusc i) ]|.
   rewrite - (big_mkord _ (fun i => if (b == fusc i) then 1 else 0)).
   have qa: 0 <= 2^n by [].
   have qb: 2^n <= m'.+1 by rewrite mpp /m expn2S double_le1.
-  rewrite (big_cat_nat _ _ _ qa qb) /= big1_seq.
+  rewrite (@big_cat_nat _ _ _ _ _ _ _ _ qa qb) /= big1_seq.  (* FIXME: replace with (big_cat_nat qa qb) when requiring MC >= 2.4.0 *)
     by rewrite add0n big_mkcond /= /x mpp; apply: eq_big_nat => i /andP[->].
   by move => i; rewrite mem_iota add0n subn0 ltnNge => /and3P [->] //.
 move => ->; clear x; apply: eq_card => a; rewrite inE;  apply/idP/imsetP.