Compat Coq 8.19 MC 2.2

math-comp · Jan 31, 2024 · e15d64e · e15d64e
1 parent 2368d83
commit e15d64e
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 13 deletions.
diff --git a/theories/Basic/unitriginv.v b/theories/Basic/unitriginv.v
@@ -224,7 +224,7 @@ Qed.
 Lemma Minv_uni t : Minv t t = 1.
 Proof.
 have [Muni Mtrig] := unitrigP _ Munitrig.
-have:= Minvr t t; rewrite eq_refl /= -[1%:R]/1 => <-.
+have:= Minvr t t; rewrite eq_refl /= mulr1n => <-.
 rewrite (bigID (fun v => v <= t)%O) /= [X in _ + X]big1 ?addr0; first last.
   by move=> v /(contraR (@Mtrig _ _))/eqP ->; rewrite mul0r.
 rewrite (bigID (fun v => t <= v)%O) /= [X in _ + X]big1 ?addr0; first last.

diff --git a/theories/LRrule/Greene.v b/theories/LRrule/Greene.v
@@ -503,7 +503,7 @@ Qed.
 Lemma Greene_rel_t_sup k : Greene_rel_t k <= N.
 Proof using.
 rewrite /Greene_rel_t /=; apply/bigmax_leqP => P _.
-move: (cover P) => cover {P}; rewrite -{5}[N]card_ord.
+move: (cover P) => cover {P}; rewrite -[N in _ <= N]card_ord.
 exact: max_card.
 Qed.
 
@@ -641,7 +641,7 @@ rewrite (_ : map _ (map rsh _) = nseq N false); first last.
   apply: (@eq_from_nth _ false); first by rewrite size_map size_enum_ord size_nseq.
   move=> i; rewrite size_map size_enum_ord => Hi.
   rewrite nth_nseq Hi /= (nth_map (Ordinal Hi)) /=; last by rewrite size_enum_ord.
-  by rewrite inE inE /= -{7}[M]addn0 ltn_add2l ltn0 andbF.
+  by rewrite inE inE /= -[M in _ < M]addn0 ltn_add2l ltn0 andbF.
 rewrite mask_false cats0 -[in RHS]map_comp; congr (mask _ V).
 apply: eq_map => i /=; rewrite inE in_setI.
 suff -> : lsh i \in [set i0 : 'I_(M+N) | i0 < M] by rewrite andbT.
@@ -985,7 +985,7 @@ elim: sh => [// | s0 sh IHsh] /=.
 rewrite imset_comp card_imset; last exact: cast_ord_inj.
 rewrite card_imset; last exact: rshift_inj.
 rewrite card_ord; congr (_ :: _).
-rewrite -map_comp -{19}IHsh; apply: eq_map.
+rewrite -map_comp -{}[RHS]IHsh; apply: eq_map.
 move=> S /=; rewrite imset_comp.
 rewrite card_imset; last exact: cast_ord_inj.
 by rewrite card_imset; last exact: lshift_inj.
@@ -1042,8 +1042,8 @@ elim: sh => [/= | s0 sh /= IHsh]; first by rewrite /trivIseq => i j /= /andP[].
 rewrite /trivIseq size_shcols_cons => i j /andP[Hij Hj].
 have Hi := ltn_trans Hij Hj.
 rewrite /disjoint; apply/pred0P => l /=; apply/negP => /andP[].
-rewrite (nth_map (Ordinal Hi)); last by rewrite size_enum_ord.
-rewrite (nth_map (Ordinal Hj)); last by rewrite size_enum_ord.
+rewrite [nth _ _ i](nth_map (Ordinal Hi)); last by rewrite size_enum_ord.
+rewrite [nth _ _ j](nth_map (Ordinal Hj)); last by rewrite size_enum_ord.
 rewrite !nth_enum_ord //=.
 rewrite in_setU1 => /orP[].
 - move/eqP => ->; rewrite in_setU1 => /orP[]; rewrite /sym_cast /=.
@@ -1279,7 +1279,7 @@ Lemma extract_tabcols_rec i :
 Proof using.
 move => Hi; rewrite /= !extractmaskE tabcols_cons enumIsize_to_word /=.
 rewrite (nth_map (Ordinal Hi)); last by rewrite size_enum_ord.
-rewrite nth_enum_ord //= {13}to_word_cons.
+rewrite nth_enum_ord //= [X in mask _ X]to_word_cons.
 rewrite nth_ord_ltn map_cat mask_cat; last by rewrite 2!size_map size_enum_ord.
 rewrite -map_comp.
 set fr := (X in rcons (mask (map X _) _)).

diff --git a/theories/LRrule/Greene_inv.v b/theories/LRrule/Greene_inv.v
@@ -1082,7 +1082,7 @@ rewrite /S'; move /extract_cut ->.
 rewrite -cats1 -[X in _ = _ ++ X]cats0 -[tnth _ _ :: _]cat1s.
 congr ((extract (in_tuple x) _) ++ _ ++ _).
 - apply/setP => i; rewrite !inE.
-  case (boolP (i \in S)) => //= _.
+  case: (boolP (i \in S)) => //= _.
   case: (ltnP i (size u).+1); last by rewrite andbF.
   by move/ltnW ->.
 - by rewrite (tnth_nth a) /x /=; elim: u.
@@ -1106,7 +1106,7 @@ congr (_ ++ _ ++ (extract (in_tuple x) _)).
   by have:= leq_trans H2 H1; rewrite ltnn.
 - by rewrite (tnth_nth a) /x /=; elim: u.
 - apply/setP => i; rewrite !inE.
-  case (boolP (i \in S)) => //= _.
+  case: (boolP (i \in S)) => //= _.
   case: (ltnP (size u).+2 i); last by rewrite andbF.
   by move/ltnW ->.
 Qed.
@@ -1120,7 +1120,7 @@ have : posb \in T' by rewrite /T' !inE leqnn Hposb.
 move /extract_cut ->; rewrite -cats1 -[[:: b]]cats0 -[tnth _ _ :: _]cat1s.
 congr ((extract (in_tuple x) _) ++ _ ++ _).
 - apply/setP => i; rewrite !inE.
-  case (boolP (i \in T)) => //= _.
+  case: (boolP (i \in T)) => //= _.
   case: (ltnP i (size u)); last by rewrite andbF.
   by move/ltnW ->.
 - by rewrite (tnth_nth a) /x /=; elim: u.
@@ -1144,7 +1144,7 @@ congr (_ ++ _ ++ (extract (in_tuple x) _)).
   by have:= leq_trans H2 H1; rewrite ltnn.
 - by rewrite (tnth_nth a) /x /=; elim: u.
 - apply/setP => i; rewrite !inE.
-  case (boolP (i \in T)) => //= Hi.
+  case: (boolP (i \in T)) => //= Hi.
   case: (ltnP (size u).+2 i).
   + by move/ltnW/ltnW => H; rewrite H (ltnW H).
   + move=> Hi1; apply/negP => /andP[_ H2].

diff --git a/theories/MPoly/antisym.v b/theories/MPoly/antisym.v
@@ -619,7 +619,8 @@ move/(_ i) : H => /=.
 rewrite /rho !mnm_tnth !tnth_mktuple !mnm_tnth !tnth_mktuple !subn1 => H.
 rewrite -[LHS]rev_ordK -[RHS]rev_ordK; congr rev_ord.
 apply val_inj => /=; rewrite !subnS.
-by have:= ltn_ord i => /ltn_predK {1 5}<-; rewrite !subSKn.
+have/ltn_predK neq11 := ltn_ord i.
+by rewrite -[X in (X - _)%N]neq11 -[X in (X - i)%N]neq11 !subSKn.
 Qed.
 
 End AlternIDomain.

diff --git a/theories/SymGroup/presentSn.v b/theories/SymGroup/presentSn.v
@@ -1395,7 +1395,7 @@ Corollary genfun_length n :
 Proof.
 case: n => [|n].
   rewrite (big_pred1_id _ _ (i := 1%g)); first last.
-    by move=> s; rewrite permS0 /= eq_refl.
+    by move=> s; rewrite !permS0 /= eq_refl.
   by rewrite addr0 length1 expr0 big_mkord big_ord0.
 rewrite (reindex _ (onW_bij _ (prods_codesz_bij n))) /=.
 under eq_bigr => i _ do