Rm notation 2 in signed.v

.github/workflows/docker-action.yml

@@ -15,20 +15,13 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.15.0-coq-8.14'
           - 'mathcomp/mathcomp:1.15.0-coq-8.15'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
           - 'mathcomp/mathcomp:1.16.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
-          - 'mathcomp/mathcomp-dev:coq-8.14'
-          - 'mathcomp/mathcomp-dev:coq-8.15'
-          - 'mathcomp/mathcomp-dev:coq-8.16'
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

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

coq-mathcomp-analysis.opam

@@ -19,7 +19,7 @@ build: [make "-C" "theories" "-j%{jobs}%"]
 install: [make "-C" "theories" "install"]
 depends: [
   "coq-mathcomp-classical" { = version}
-  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.18~") | (= "dev") }
+  "coq-mathcomp-solvable" { (>= "1.15.0" & < "1.18~") | (= "dev") }
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
 ]

theories/ereal.v

@@ -1159,7 +1159,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 ltr_subr_addl -!mulr2n -(mulr_natl e%:num).
-    by rewrite -{1}(mulr1 2) => ?; rewrite -(@ltr_pmul2l _ 2).
+    by rewrite -{1}(mulr1 2%:R) => ?; rewrite -(@ltr_pmul2l _ 2).
   have Aoo : setT `\ -oo `<=` A.
     move=> x [_]; rewrite /set1 /= => xnoo; apply reA.
     case: x xnoo => [r' _ | _ |//].
@@ -1212,7 +1212,7 @@ move: re1; rewrite le_eqVlt => /orP[re1|re1].
   have e1 : (1 < e%:num)%R.
     move: reN1.
     rewrite re1 -addrA -opprD ltr_subl_addl ltr_subr_addl -!mulr2n.
-    rewrite -(mulr_natl e%:num) -{1}(mulr1 2) => ?.
+    rewrite -(mulr_natl e%:num) -{1}(mulr1 2%:R) => ?.
     by rewrite -(@ltr_pmul2l _ 2).
   have Aoo : (setT `\ +oo `<=` A).
     move=> x [_]; rewrite /set1 /= => xpoo; apply reA.

theories/exp.v

@@ -211,7 +211,7 @@ suff Cc : lim (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> lim (series s).
     apply: is_cvg_pseries_inside Ck _.
     rewrite (le_lt_trans (ler_norm_add _ _))// -(subrK  `|x| `|K|) ltr_add2r.
     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_pdivr_mulr // mulr2n mulrDr mulr1.
@@ -233,7 +233,7 @@ suff Cc : lim
     apply: is_cvg_pseries_inside Ck _.
     rewrite (le_lt_trans (ler_norm_add _ _))// -(subrK  `|x| `|K|) ltr_add2r.
     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_pdivr_mulr // mulr2n mulrDr mulr1.
@@ -256,7 +256,7 @@ suff Cc : lim
   have -> : h^-1 *: series (shx h - sx) = series (h^-1 *: (shx h - sx)).
     by apply/funext => i; rewrite /series /= -scaler_sumr.
   exact/esym/cvg_lim.
-pose r := (`|x| + `|K|) / 2.
+pose r := (`|x| + `|K|) / 2%:R.
 have xLr : `|x| < r by rewrite ltr_pdivl_mulr // mulr2n mulrDr mulr1 ltr_add2l.
 have rLx : r < `|K| by rewrite ltr_pdivr_mulr // mulr2n mulrDr mulr1 ltr_add2r.
 have r_gt0 : 0 < r by apply: le_lt_trans xLr.

theories/numfun.v

@@ -463,7 +463,7 @@ have [xR|xR] := lerP (1/3 * M%:num) (f x).
   by rewrite ler_subl_addl -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 ler_sub// -mulNr ltW.
 by rewrite (ler_add (ltW _))// ler_oppl -mulNr.
 Qed.

theories/signed.v

@@ -98,7 +98,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   *)
@@ -306,7 +305,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.