Rm notation 2 in signed.v (math-comp#999)

* Remove no longer useful notation since MC 1.15

* [CI] Update Docker CI

CHANGELOG_UNRELEASED.md

@@ -100,6 +100,12 @@
 
 ### Removed
 
+- in `signed.v`:
+  + specific notation for `2%:R`,
+    now subsumed by number notations in MC >= 1.15
+    Note that when importing ssrint, `2` now denotes `2%:~R` rather than `2%:R`,
+    which are convertible but don't have the same head constant.
+
 ### Infrastructure
 
 ### Misc

theories/ereal.v

@@ -1155,7 +1155,7 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1)%R.
     by apply (@nbhs_fin_out_below _ e) => //; rewrite reN1 addrAC subrr sub0r.
   have e1 : (1 < e%:num)%R.
     move: re1; rewrite reN1 addrAC ltrBrDl -!mulr2n -(mulr_natl e%:num).
-    by rewrite -{1}(mulr1 2) => ?; rewrite -(@ltr_pM2l _ 2).
+    by rewrite -{1}(mulr1 2%:R) => ?; rewrite -(@ltr_pM2l _ 2).
   have Aoo : setT `\ -oo `<=` A.
     move=> x [_]; rewrite /set1 /= => xnoo; apply reA.
     case: x xnoo => [r' _ | _ |//].
@@ -1208,7 +1208,7 @@ move: re1; rewrite le_eqVlt => /orP[re1|re1].
   have e1 : (1 < e%:num)%R.
     move: reN1.
     rewrite re1 -addrA -opprD ltrBlDl ltrBrDl -!mulr2n.
-    rewrite -(mulr_natl e%:num) -{1}(mulr1 2) => ?.
+    rewrite -(mulr_natl e%:num) -{1}(mulr1 2%:R) => ?.
     by rewrite -(@ltr_pM2l _ 2).
   have Aoo : (setT `\ +oo `<=` A).
     move=> x [_]; rewrite /set1 /= => xpoo; apply reA.

theories/exp.v

@@ -215,7 +215,7 @@ suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s).
     apply: is_cvg_pseries_inside Ck _.
     rewrite (le_lt_trans (ler_normD _ _))// -(subrK  `|x| `|K|) ltrD2r.
     near: h.
-    apply/nbhs_ballP => /=; exists ((`|K| - `|x|) /2) => /=.
+    apply/nbhs_ballP => /=; exists ((`|K| - `|x|) /2%:R) => /=.
       by rewrite divr_gt0 // subr_gt0.
     move=> t; rewrite /ball /= sub0r normrN => H tNZ.
     rewrite (lt_le_trans H)// ler_pdivrMr // mulr2n mulrDr mulr1.
@@ -238,7 +238,7 @@ suff Cc : limn
     apply: is_cvg_pseries_inside Ck _.
     rewrite (le_lt_trans (ler_normD _ _))// -(subrK  `|x| `|K|) ltrD2r.
     near: h.
-    apply/nbhs_ballP => /=; exists ((`|K| - `|x|) /2) => /=.
+    apply/nbhs_ballP => /=; exists ((`|K| - `|x|) / 2%:R) => /=.
       by rewrite divr_gt0 // subr_gt0.
     move=> t; rewrite /ball /= sub0r normrN => H tNZ.
     rewrite (lt_le_trans H)// ler_pdivrMr // mulr2n mulrDr mulr1.
@@ -262,8 +262,8 @@ suff Cc : limn
     by apply/funext => i; rewrite /series /= -scaler_sumr.
   exact/esym/cvg_lim.
 pose r := (`|x| + `|K|) / 2.
-have xLr : `|x| < r by rewrite ltr_pdivlMr // mulr2n mulrDr mulr1 ltrD2l.
-have rLx : r < `|K| by rewrite ltr_pdivrMr // mulr2n mulrDr mulr1 ltrD2r.
+have xLr : `|x| < r by rewrite ltr_pdivlMr // mulrDr mulr1 ltrD2l.
+have rLx : r < `|K| by rewrite ltr_pdivrMr // mulrDr mulr1 ltrD2r.
 have r_gt0 : 0 < r by apply: le_lt_trans xLr.
 have rNZ : r != 0by case: ltrgt0P r_gt0.
 apply: (@lim_cvg_to_0_linear _

theories/lebesgue_integral.v

@@ -4867,7 +4867,7 @@ Proof.
 move=> Afin mfA bdA; apply/integrableP; split; first exact/EFin_measurable_fun.
 have [M [_ mrt]] := bdA; apply: le_lt_trans.
   apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp.
-  by apply: aeW => z Az; rewrite lee_fin mrt// ltr_spaddr// ler_norm.
+  by apply: aeW => z Az; rewrite lee_fin mrt// ltr_pwDr// ler_norm.
 by rewrite lte_mul_pinfty.
 Qed.
 
@@ -4961,9 +4961,9 @@ Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo.
 Proof.
 move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]].
 have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R.
-  by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm.
+  by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_pwDr// ler_norm.
 rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=.
-by rewrite lebesgue_measure_itv hlength_itv/= lte_fin gtr_opp// EFinD ltry.
+by rewrite lebesgue_measure_itv hlength_itv/= lte_fin gtrN// EFinD ltry.
 Qed.
 
 Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) :

theories/numfun.v

@@ -461,7 +461,7 @@ have [xR|xR] := lerP (1/3 * M%:num) (f x).
   by rewrite lerBlDl -2!mulrDl nat1r divrr ?mul1r// unitfE.
 have /andP[ng3 pg3] : -(1/3) * M%:num <= g x <= 1/3 * M%:num.
   by apply: grng; exists x.
-rewrite (natrD _ 1 1) !mulrDl; apply/andP; split.
+rewrite (intrD _ 1 1) !mulrDl; apply/andP; split.
   by rewrite opprD lerB// -mulNr ltW.
 by rewrite (lerD (ltW _))// lerNl -mulNr.
 Qed.

theories/signed.v

@@ -99,7 +99,6 @@ From mathcomp Require Import mathcomp_extra.
 (*                  main use case is to trigger typeclass inference in the    *)
 (*                  body of a ssreflect have := !! body.                      *)
 (*                  Credits: Enrico Tassi.                                    *)
-(*             2 == notation for 2%:R.                                        *)
 (*                                                                            *)
 (* --> A number of canonical instances are provided for common operations, if *)
 (* your favorite operator is missing, look below for examples on how to add   *)
@@ -307,7 +306,6 @@ Notation "x %:posnum" := (@num _ _ 0%R !=0 >=0 x) : ring_scope.
 Definition nonneg (R : numDomainType) of phant R := {>= 0%R : R}.
 Notation "{ 'nonneg' R }" := (@nonneg _ (Phant R))  : ring_scope.
 Notation "x %:nngnum" := (@num _ _ 0%R ?=0 >=0 x) : ring_scope.
-Notation "2" := 2%:R : ring_scope.
 Arguments r {disp T x0 nz cond}.
 End Exports.
 End Signed.