From 7588356c33b8f46a5030072193801576b7a2feaf Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi <pi8027@gmail.com>
Date: Tue, 10 Nov 2020 18:54:37 +0900
Subject: [PATCH 1/6] Compatible with MathComp master (and hopefully 1.12)

---
 config.nix            |  6 +--
 theories/derive.v     | 27 +++++++-------
 theories/normedtype.v | 87 ++++++++++++++++++-------------------------
 3 files changed, 53 insertions(+), 67 deletions(-)

diff --git a/config.nix b/config.nix
index 7c30f74dc..1daa16d79 100644
--- a/config.nix
+++ b/config.nix
@@ -1,6 +1,6 @@
 {
   coq = "8.11";
-  mathcomp = "mathcomp-1.11.0";
-  mathcomp-real-closed = "1.1.1";
-  mathcomp-finmap = "1.5.0";
+  mathcomp = "mathcomp-1.12.0";
+  mathcomp-real-closed = "1.1.2";
+  mathcomp-finmap = "1.5.1";
 }
diff --git a/theories/derive.v b/theories/derive.v
index 27cf6c427..ec5c8d13f 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1312,7 +1312,7 @@ Proof.
 move=> leab fcont; set imf := [set t | (f @` [set x | x \in `[a, b]]) t].
 have imf_sup : has_sup imf.
   split.
-    by exists (f a) => //; rewrite /imf; apply/imageP; rewrite /= inE /= lexx.
+    by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
   have [M [Mreal imfltM]] : bounded_set (f @` [set x | x \in `[a, b]] : set R^o).
     apply/compact_bounded/continuous_compact; last exact: segment_compact.
     by move=> ?; rewrite inE => /fcont.
@@ -1430,9 +1430,9 @@ apply/eqP; rewrite eq_le; apply/andP; split.
     by rewrite invr_ge0; apply: ltW; near: h; exists 1.
   rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
   exists (b - c); first by rewrite /= subr_gt0 (itvP cab).
-  move=> h; rewrite /= distrC subr0.
-  move=> /(le_lt_trans (ler_norm _)); rewrite ltr_subr_addr inE/= => ->.
-  by move=> /ltr_spsaddl -> //; rewrite (itvP cab).
+  move=> h; rewrite /= distrC subr0 /= in_itv /= -ltr_subr_addr.
+  move=> /(le_lt_trans (ler_norm _)) -> /ltr_spsaddl -> //.
+  by rewrite (itvP cab).
 rewrite ['D_1 f c]cvg_at_leftE; last exact: fdrvbl.
 apply: le0r_cvg_map; last first.
   have /fdrvbl dfc := cab; rewrite -(@cvg_at_leftE _ _ (fun h => h^-1 *: ((f \o shift c) _ - f c))) //.
@@ -1444,7 +1444,7 @@ near=> h; apply: mulr_le0.
 rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
 exists (c - a); first by rewrite /= subr_gt0 (itvP cab).
 move=> h; rewrite /= distrC subr0.
-move=> /ltr_normlP []; rewrite ltr_subr_addl ltr_subl_addl inE/= => -> _.
+move=> /ltr_normlP []; rewrite ltr_subr_addl ltr_subl_addl in_itv /= => -> _.
 by move=> /ltr_snsaddl -> //; rewrite (itvP cab).
 Grab Existential Variables. all: end_near. Qed.
 
@@ -1471,24 +1471,24 @@ case: (pselect ([set a; b] cmax))=> [cmaxeaVb|]; last first.
   move=> /asboolPn; rewrite asbool_or => /norP.
   move=> [/asboolPn/eqP cnea /asboolPn/eqP cneb].
   have {}cmaxab : cmax \in `]a, b[.
-    by rewrite inE/= !lt_def !(itvP cmaxab) cnea eq_sym cneb.
+    by rewrite in_itv /= !lt_def !(itvP cmaxab) cnea eq_sym cneb.
   exists cmax => //; apply: derive1_at_max (ltW ltab) fdrvbl cmaxab _ => t tab.
-  by apply: fcmax; rewrite inE/= !ltW // (itvP tab).
+  by apply: fcmax; rewrite in_itv /= !ltW // (itvP tab).
 have [cmin cminab fcmin] := EVT_min (ltW ltab) fcont.
 case: (pselect ([set a; b] cmin))=> [cmineaVb|]; last first.
   move=> /asboolPn; rewrite asbool_or => /norP.
   move=> [/asboolPn/eqP cnea /asboolPn/eqP cneb].
   have {}cminab : cmin \in `]a, b[.
-    by rewrite inE/= !lt_def !(itvP cminab) cnea eq_sym cneb.
+    by rewrite in_itv /= !lt_def !(itvP cminab) cnea eq_sym cneb.
   exists cmin => //; apply: derive1_at_min (ltW ltab) fdrvbl cminab _ => t tab.
-  by apply: fcmin; rewrite inE/= !ltW // (itvP tab).
+  by apply: fcmin; rewrite in_itv /= !ltW // (itvP tab).
 have midab : (a + b) / 2 \in `]a, b[ by apply: mid_in_itvoo.
 exists ((a + b) / 2) => //; apply: derive1_at_max (ltW ltab) fdrvbl (midab) _.
 move=> t tab.
 suff fcst : forall s, s \in `]a, b[ -> f s = f cmax by rewrite !fcst.
 move=> s sab.
-apply/eqP; rewrite eq_le fcmax; last by rewrite inE/= !ltW ?(itvP sab).
-suff -> : f cmax = f cmin by rewrite fcmin // inE/= !ltW ?(itvP sab).
+apply/eqP; rewrite eq_le fcmax; last by rewrite in_itv /= !ltW ?(itvP sab).
+suff -> : f cmax = f cmin by rewrite fcmin // in_itv /= !ltW ?(itvP sab).
 by case: cmaxeaVb => ->; case: cmineaVb => ->.
 Qed.
 
@@ -1512,7 +1512,7 @@ have gaegb : g a = g b.
     by rewrite mul1r addrCA subrr addr0.
   by apply: lt0r_neq0; rewrite subr_gt0.
 have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb.
-exists c; first by apply/andP; split; apply/ltW; rewrite (itvP cab).
+exists c; first by rewrite in_itv /= ltW (itvP cab).
 have /fdrvbl dfc := cab; move/@derive_val: dgc0; rewrite deriveB //; last first.
   exact/derivable1_diffP.
 move/eqP; rewrite [X in _ - X]deriveE // derive_val diff_val scale1r subr_eq0.
@@ -1526,7 +1526,8 @@ Lemma ler0_derive1_nincr (R : realType) (f : R^o -> R^o) (a b : R) :
   forall x y, a <= x -> x <= y -> y <= b -> f y <= f x.
 Proof.
 move=> fdrvbl dfle0 x y leax lexy leyb; rewrite -subr_ge0.
-have itvW : {subset `[x, y] <= `[a, b]} by apply/subitvP; rewrite /= leyb leax.
+have itvW : {subset `[x, y] <= `[a, b]}.
+  by apply/subitvP; rewrite /<=%O /= /<=%O /= leyb leax.
 have fdrv z : z \in `]x, y[ -> is_derive (z : R^o) 1 f (f^`()z).
   rewrite inE => /andP [/ltW lexz /ltW lezy].
   apply: DeriveDef; last by rewrite derive1E.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index e3e3f3b37..de1504ff7 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -330,10 +330,9 @@ Lemma in_segment_addgt0Pr (R : numFieldType) (x y z : R) :
   reflect (forall e, e > 0 -> y \in `[(x - e), (z + e)]) (y \in `[x, z]).
 Proof.
 apply/(iffP idP)=> [xyz _/posnumP[e] | xyz_e].
-  rewrite inE/=; apply/andP; split; last by rewrite ler_paddr // (itvP xyz).
-  by rewrite ler_subl_addr ler_paddr // (itvP xyz).
-rewrite inE/=; apply/andP.
-by split; apply/ler_addgt0Pr => ? /xyz_e /andP /= []; rewrite ler_subl_addr.
+  by rewrite in_itv /= ler_subl_addr !ler_paddr // (itvP xyz).
+by rewrite in_itv /= ; apply/andP; split; apply/ler_addgt0Pr => ? /xyz_e;
+  rewrite in_itv /= ler_subl_addr => /andP [].
 Qed.
 
 Lemma in_segment_addgt0Pl (R : numFieldType) (x y z : R) :
@@ -1034,7 +1033,7 @@ Lemma Rhausdorff (R : realFieldType) : hausdorff [topologicalType of R^o].
 Proof.
 move=> x y clxy; apply/eqP; rewrite eq_le.
 apply/(@in_segment_addgt0Pr _ x _ x) => _ /posnumP[e].
-rewrite inE -ler_distl; set he := (e%:num / 2)%:pos.
+rewrite in_itv /= -ler_distl; set he := (e%:num / 2)%:pos.
 have [z []] := clxy _ _ (nbhsx_ballx x he) (nbhsx_ballx y he).
 move=> zx_he yz_he.
 rewrite -(subrKA z) (le_trans (ler_norm_add _ _) _)// ltW //.
@@ -2254,37 +2253,32 @@ rewrite [X in closed X](_ : (eq^~ _) = ~` (xpredC (eq_op^~ y))).
 by rewrite predeqE /setC => x /=; rewrite (rwP eqP); case: eqP; split.
 Qed.
 
-(* TODO: move after rebase on mathcomp 1.12?  *)
-Definition isBOpen (b : itv_bound R) :=
-  if b is BOpen _ then true else false.
+Definition bound_side d (T : porderType d) (c : bool) (x : itv_bound T) :=
+  if x is BSide c' _ then c == c' else false.
 
-Definition isBClosed (b : itv_bound R) :=
-  if b is BOpen_if false _ then true else false.
-
-Lemma interval_open a b : ~~ isBClosed a -> ~~ isBClosed b ->
+Lemma interval_open a b : ~~ bound_side true a -> ~~ bound_side false b ->
   open [set x : R^o | x \in Interval a b].
 Proof.
-move: a b => [[]//a|] [[]//b|] _ _.
+move: a b => [[]a|[]] [[]b|[]]// _ _.
 - have -> : [set x | a < x < b] = [set x | a < x] `&` [set x | x < b].
     by rewrite predeqE => r; rewrite /mkset; split => [/andP[? ?] //|[-> ->]].
   by apply openI; [exact: open_gt | exact: open_lt].
-- rewrite (_ : [set x | x \in _] = [set x : R^o | x > a]) //.
-  by rewrite predeqE => r; split => //; rewrite /mkset ?(inE,lersifT,andbT).
+- by under eq_set do rewrite itv_ge// inE.
+- by under eq_set do rewrite in_itv andbT/=; exact: open_gt.
 - exact: open_lt.
 - by rewrite (_ : mkset _ = setT); [exact: openT | rewrite predeqE].
 Qed.
 
-Lemma interval_closed a b : ~~ isBOpen a -> ~~ isBOpen b ->
+Lemma interval_closed a b : ~~ bound_side false a -> ~~ bound_side true b ->
   closed [set x : R^o | x \in Interval a b].
 Proof.
-move: a b => [[]//a|] [[]//b|] _ _.
+move: a b => [[]a|[]] [[]b|[]]// _ _;
+  do ?by under eq_set do rewrite itv_ge// inE falseE; apply: closed0.
 - have -> : [set x | x \in `[a, b]] = [set x | x >= a] `&` [set x | x <= b].
-    by rewrite predeqE => ?; rewrite /= inE; split=> [/andP [] | /= [->]].
+    by rewrite predeqE => ?; rewrite /= in_itv/=; split=> [/andP[]|[->]].
   by apply closedI; [exact: closed_ge | exact: closed_le].
-- rewrite (_ : mkset _ = [set x : R^o | x >= a]); first exact :closed_ge.
-  by rewrite predeqE => r; split => //; rewrite /mkset ?(inE,lersifT,andbT).
+- by under eq_set do rewrite in_itv andbT/=; exact: closed_ge.
 - exact: closed_le.
-- by rewrite (_ : mkset _ = setT); [exact: closedT|rewrite predeqE].
 Qed.
 
 End open_closed_sets.
@@ -2349,16 +2343,9 @@ Qed.
 
 Lemma interval_is_interval (i : interval R) : is_interval [set x | x \in i].
 Proof.
-move: i => [[[] i|] [[] j|]] //= x y; rewrite /mkset !(inE,lersifT,lersifF);
-  move=> /andP[ax ?] /andP[? yb] z /andP[? ?]; rewrite !(inE,lersifT,lersifF).
-by rewrite (lt_trans ax) // (lt_trans _ yb).
-by rewrite (lt_trans ax) // (le_trans (ltW _) yb).
-by rewrite (lt_trans ax).
-by rewrite (le_trans ax (ltW _)) // (lt_trans _ yb).
-by rewrite (le_trans ax (ltW _)) // (le_trans (ltW _) yb).
-by rewrite (le_trans ax (ltW _)).
-by rewrite (lt_trans _ yb).
-by rewrite (le_trans (ltW _) yb).
+by case: i => -[[]a|[]] [[]b|[]] // x y /=; do ?[by rewrite ?itv_ge//];
+   move=> xi yi z; rewrite -[x < z < y]/(z \in `]x, y[); apply/subitvP;
+   rewrite subitvE /Order.le/= ?(itvP xi, itvP yi).
 Qed.
 
 End interval.
@@ -2448,7 +2435,7 @@ Proof.
 move=> iX bX aX; rewrite eqEsubset; split=> [r Xr|].
   apply/andP; split;
     [exact: left_bounded_interior|exact: right_bounded_interior].
-rewrite -open_subsetE; last exact: (@interval_open _ (BOpen _) (BOpen _)).
+rewrite -open_subsetE; last exact: (@interval_open _ (BRight _) (BLeft _)).
 move=> r /andP[iXr rsX].
 have [/set0P X0|/negPn/eqP X0] := boolP (X != set0); last first.
   by move: (lt_trans iXr rsX); rewrite X0 inf_out ?sup_out ?ltxx // => - [[]].
@@ -2461,31 +2448,30 @@ by rewrite opprB addrCA subrr addr0 => rf; apply: (iX _ _ Xe Xf); rewrite er rf.
 Qed.
 
 Definition Rhull (X : set R) : interval R := Interval
-  (if `[< has_lbound X >] then BOpen_if (~~ `[< X (inf X) >]) (inf X)
-                          else BInfty _)
-  (if `[< has_ubound X >] then BOpen_if (~~ `[< X (sup X) >]) (sup X)
-                          else BInfty _).
+  (if `[< has_lbound X >] then BSide `[< X (inf X) >] (inf X)
+                          else BInfty _ true)
+  (if `[< has_ubound X >] then BSide (~~ `[< X (sup X) >]) (sup X)
+                          else BInfty _ false).
 
 Lemma sub_Rhull (X : set R) : X `<=` [set x | x \in Rhull X].
 Proof.
-move=> x Xx/=; rewrite inE/=.
+move=> x Xx/=; rewrite in_itv/=.
 case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=.
 + by case: asboolP => ?; case: asboolP => ? //=;
-     rewrite !(lersifF, lersifT, sup_ub, inf_lb, sup_ub_strict, inf_lb_strict).
-+ by case: asboolP => XinfX; rewrite !(lersifF, lersifT);
+     rewrite !(lteifF, lteifT, sup_ub, inf_lb, sup_ub_strict, inf_lb_strict).
++ by case: asboolP => XinfX; rewrite !(lteifF, lteifT);
      [rewrite inf_lb | rewrite inf_lb_strict].
-+ by case: asboolP => XsupX; rewrite !(lersifF, lersifT);
++ by case: asboolP => XsupX; rewrite !(lteifF, lteifT);
      [rewrite sup_ub | rewrite sup_ub_strict].
 Qed.
 
-
 Lemma is_intervalP (X : set R) : is_interval X <-> X = [set x | x \in Rhull X].
 Proof.
 split=> [iX|->]; last exact: interval_is_interval.
-rewrite predeqE => x /=; split; [exact: sub_Rhull | rewrite inE/=].
+rewrite predeqE => x /=; split; [exact: sub_Rhull | rewrite in_itv/=].
 case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=.
 - case: asboolP => XinfX; case: asboolP => XsupX;
-    rewrite !(lersifF, lersifT).
+    rewrite !(lteifF, lteifT).
   + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx].
     rewrite le_eqVlt => /orP[/eqP -> //|xsupX].
     apply: (@interior_subset [topologicalType of R^o]).
@@ -2498,7 +2484,7 @@ case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=.
     by rewrite interval_bounded_interior // /mkset infXx.
   + move=> ?; apply: (@interior_subset [topologicalType of R^o]).
     by rewrite interval_bounded_interior // /mkset infXx.
-- case: asboolP => XinfX; rewrite !(lersifF, lersifT, andbT).
+- case: asboolP => XinfX; rewrite !(lteifF, lteifT, andbT).
   + rewrite le_eqVlt => /orP[/eqP<-//|infXx].
     apply: (@interior_subset [topologicalType of R^o]).
     by rewrite interval_right_unbounded_interior.
@@ -2581,7 +2567,6 @@ split => [cE x y Ex Ey z /andP[xz zy]|].
 Qed.
 End interval_realType.
 
-
 Section segment.
 Variable R : realType.
 
@@ -2614,7 +2599,7 @@ apply: segment_connected.
   rewrite openE => /(_ _ fx) [e egt0 xe_fi]; exists e => // y xe_y.
   exists D' => //; split; last by exists i => //; apply/xe_fi.
   move=> z /= ayz; case: (lerP z x) => [lezx|ltxz].
-    by apply/saxUf; rewrite /= inE/= (itvP ayz) lezx.
+    by apply/saxUf; rewrite /= in_itv/= (itvP ayz) lezx.
   exists i => //; apply/xe_fi; rewrite /ball_/= distrC ger0_norm.
     have lezy : z <= y by rewrite (itvP ayz).
     rewrite ltr_subl_addl; apply: le_lt_trans lezy _; rewrite -ltr_subl_addr.
@@ -2631,7 +2616,7 @@ split=> [z axz|]; last first.
   exists i; first by rewrite /= !inE eq_refl.
   by apply/xe_fi; rewrite /ball_/= subrr normr0.
 case: (lerP z y) => [lezy|ltyz].
-  have /sayUf [j Dj fjz] : z \in `[a, y] by rewrite inE/= (itvP axz) lezy.
+  have /sayUf [j Dj fjz] : z \in `[a, y] by rewrite in_itv /= (itvP axz) lezy.
   by exists j => //=; rewrite inE orbC Dj.
 exists i; first by rewrite /= !inE eq_refl.
 apply/xe_fi; rewrite /ball_/= ger0_norm; last first.
@@ -2665,9 +2650,9 @@ move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b ->
     by move=> x /fcont; apply: (@continuousN _ [normedModType R of R^o]).
   by rewrite ler_oppr opprK ler_oppr opprK andbC.
 move=> /andP[]; rewrite le_eqVlt => /orP [/eqP<- _|ltfav].
-  by exists a => //; rewrite inE/= lexx leab.
+  by exists a => //; rewrite in_itv /= lexx leab.
 rewrite le_eqVlt => /orP [/eqP->|ltvfb].
-  by exists b => //; rewrite inE/= lexx leab.
+  by exists b => //; rewrite in_itv /= lexx leab.
 set A := [set c | (c <= b) && (f c <= v)].
 have An0 : nonempty A by exists a; apply/andP; split=> //; apply: ltW.
 have supA : has_sup A by split=> //; exists b; apply/ubP => ? /andP [].
@@ -2702,8 +2687,8 @@ rewrite ler_add2r ltW //; suff : forall t, t \in `](sup A), b] -> v < f t.
     by move: lefsupv; rewrite leNgt -besup ltvfb.
   move=> t lttb ltsupt; move: lttb; rewrite /= distrC.
   by rewrite gtr0_norm ?subr_gt0 // ltr_add2r; apply: ltW.
-move=> t /andP [ltsupt /= letb]; rewrite ltNge; apply/negP => leftv.
-move: ltsupt => /=; rewrite ltNge => /negP; apply.
+move=> t; rewrite in_itv /=; case/andP => ltsupt letb.
+apply/contra_lt: ltsupt => leftv.
 by move/ubP : (sup_upper_bound supA); apply; rewrite /A/= leftv letb.
 Grab Existential Variables. all: end_near. Qed.
 

From c28b89b44a093027ffeb6eaae63ed0c6413a4d15 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sat, 5 Dec 2020 23:44:38 +0900
Subject: [PATCH 2/6] so that it compiles with mathcomp 1.12

---
 theories/forms.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/forms.v b/theories/forms.v
index bed94efdd..b2e505a47 100644
--- a/theories/forms.v
+++ b/theories/forms.v
@@ -253,7 +253,7 @@ End BidirectionalLinearZ.
 
 End BilinearTheory.
 
-Canonical rev_mulmx (R : ringType) m n p := @RevOp _ _ _ (@mulmxr_head R m n p tt)
+Canonical rev_mulmx (R : ringType) m n p := @RevOp _ _ _ (@mulmxr R m n p)
   (@mulmx R m n p) (fun _ _ => erefl).
 
 Canonical mulmx_bilinear (R : comRingType) m n p := [bilinear of @mulmx R m n p].

From 84fb05005346a8c65247b15b1cede651cb263c11 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Wed, 9 Dec 2020 02:08:06 +0100
Subject: [PATCH 3/6] regenerate metadata

---
 .github/workflows/coq-action.yml |  4 ++--
 README.md                        | 12 ++++++------
 coq-mathcomp-analysis.opam       | 12 ++++++------
 meta.yml                         | 28 ++++++++++++++--------------
 4 files changed, 28 insertions(+), 28 deletions(-)

diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index 491406df7..e57449e75 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -15,8 +15,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.11.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2
diff --git a/README.md b/README.md
index 85c5bbc27..9fc31b638 100644
--- a/README.md
+++ b/README.md
@@ -27,12 +27,12 @@ the Coq proof-assistant and using the Mathematical Components library.
 - License: [CeCILL-C](LICENSE)
 - Compatible Coq versions: Coq 8.11 to 8.12
 - Additional dependencies:
-  - [MathComp ssreflect 1.11](https://math-comp.github.io)
-  - [MathComp fingroup 1.11](https://math-comp.github.io)
-  - [MathComp algebra 1.11](https://math-comp.github.io)
-  - [MathComp solvable 1.11](https://math-comp.github.io)
-  - [MathComp field 1.11](https://math-comp.github.io)
-  - [MathComp finmap 1.5](https://github.com/math-comp/finmap)
+  - [MathComp ssreflect 1.12](https://math-comp.github.io)
+  - [MathComp fingroup 1.12](https://math-comp.github.io)
+  - [MathComp algebra 1.12](https://math-comp.github.io)
+  - [MathComp solvable 1.12](https://math-comp.github.io)
+  - [MathComp field 1.12](https://math-comp.github.io)
+  - [MathComp finmap 1.5.1](https://github.com/math-comp/finmap)
   - [Hierarchy Builder 0.10](https://github.com/math-comp/hierarchy-builder)
 - Coq namespace: `mathcomp.analysis`
 - Related publication(s):
diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam
index 695d95883..5ea0e3dcc 100644
--- a/coq-mathcomp-analysis.opam
+++ b/coq-mathcomp-analysis.opam
@@ -16,12 +16,12 @@ build: [make "-j%{jobs}%" ]
 install: [make "install"]
 depends: [
   "coq" { (>= "8.11" & < "8.13~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-fingroup" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-algebra" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-solvable" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-field" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-finmap" { (>= "1.5.0" & < "1.6~") }
+  "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-fingroup" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-solvable" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-field" { (>= "1.12.0" & < "1.13~") }
+  "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") }
   "coq-hierarchy-builder" { (>= "0.10.0" & < "0.11~") }
 ]
 
diff --git a/meta.yml b/meta.yml
index 98d3a52c7..e53a1cd23 100644
--- a/meta.yml
+++ b/meta.yml
@@ -44,42 +44,42 @@ supported_coq_versions:
   opam: '{ (>= "8.11" & < "8.13~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.11.0-coq-8.11'
+- version: '1.12.0-coq-8.11'
   repo: 'mathcomp/mathcomp'
-- version: '1.11.0-coq-8.12'
+- version: '1.12.0-coq-8.12'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp ssreflect 1.11](https://math-comp.github.io)
+    [MathComp ssreflect 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp fingroup 1.11](https://math-comp.github.io)
+    [MathComp fingroup 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp algebra 1.11](https://math-comp.github.io)
+    [MathComp algebra 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp solvable 1.11](https://math-comp.github.io)
+    [MathComp solvable 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.12.0" & < "1.13~") }'
   description: |-
-    [MathComp field 1.11](https://math-comp.github.io)
+    [MathComp field 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-finmap
-    version: '{ (>= "1.5.0" & < "1.6~") }'
+    version: '{ (>= "1.5.1" & < "1.6~") }'
   description: |-
-    [MathComp finmap 1.5](https://github.com/math-comp/finmap)
+    [MathComp finmap 1.5.1](https://github.com/math-comp/finmap)
 - opam:
     name: coq-hierarchy-builder
     version: '{ (>= "0.10.0" & < "0.11~") }'

From b055efe0dfec41c8f541d281bd4243cc4a59b192 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 14 Dec 2020 17:50:04 +0900
Subject: [PATCH 4/6] fixes

- fixes #277
- add the same fail-on-warnings as MathComp
- fixes #259
---
 _CoqProject               |  3 +++
 theories/boolp.v          | 26 +++-----------------------
 theories/classical_sets.v |  2 ++
 theories/ereal.v          |  2 ++
 theories/landau.v         |  4 +++-
 theories/normedtype.v     | 23 ++---------------------
 theories/reals.v          |  2 ++
 theories/topology.v       |  2 +-
 8 files changed, 18 insertions(+), 46 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 68d4a3350..0d7feb0f1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,8 @@
 -arg -w
 -arg -parsing
+-arg -w -arg +undeclared-scope
+-arg -w -arg +non-primitive-record
+-arg -w -arg +undeclared-scope
 
 theories/boolp.v
 theories/ereal.v
diff --git a/theories/boolp.v b/theories/boolp.v
index 0ce11e6f6..2bbde07da 100644
--- a/theories/boolp.v
+++ b/theories/boolp.v
@@ -11,6 +11,9 @@ Set   Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope box_scope.
+Declare Scope quant_scope.
+
 (* Copy of the ssrbool shim to ensure compatibility with MathComp v1.8.0. *)
 Definition PredType : forall T pT, (pT -> pred T) -> predType T.
 exact PredType || exact mkPredType.
@@ -325,29 +328,6 @@ by case=> x bPx; apply/asboolP; exists x; apply/asboolP.
 Qed.
 
 (* -------------------------------------------------------------------- *)
-Lemma contra_not (Q P : Prop) : (Q -> P) -> ~ P -> ~ Q.
-Proof.
-move=> cb /asboolPn nb; apply/asboolPn.
-by apply: contra nb => /asboolP /cb /asboolP.
-Qed.
-
-(** subsumed by mathcomp 1.12, to be removed *)
-Lemma contra_notT (P: Prop) (b:bool) : (~~ b -> P) -> ~ P -> b.
-Proof. by case: b => //= /(_ isT) HP /(_ HP). Qed.
-
-(** subsumed by mathcomp 1.12, to be removed *)
-Lemma contra_notN (P: Prop) (b:bool) : (b -> P) -> ~ P -> ~~ b.
-Proof. rewrite -{1}[b]negbK; exact: contra_notT. Qed.
-
-(** subsumed by mathcomp 1.12, to be removed *)
-Lemma contra_not_neq (T: eqType)  (P: Prop) (x y:T) : (x = y -> P) -> ~ P -> x != y.
-Proof. by move=> imp; apply: contra_notN => /eqP. Qed.
-
-Lemma contraPnot (Q P : Prop) : (Q -> ~ P) -> P -> ~ Q.
-Proof.
-move=> cb /asboolP hb; apply/asboolPn.
-by apply: contraL hb => /asboolP /cb /asboolPn.
-Qed.
 
 Lemma contra_notP (Q P : Prop) : (~ Q -> P) -> ~ P -> Q.
 Proof.
diff --git a/theories/classical_sets.v b/theories/classical_sets.v
index be57d1fb4..edc3f7953 100644
--- a/theories/classical_sets.v
+++ b/theories/classical_sets.v
@@ -98,6 +98,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope classical_set_scope.
+
 Reserved Notation "[ 'set' x : T | P ]"
   (at level 0, x at level 99, only parsing).
 Reserved Notation "[ 'set' x | P ]"
diff --git a/theories/ereal.v b/theories/ereal.v
index 6ac2c9b14..3aa59c3c9 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -55,6 +55,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope ereal_scope.
+
 Import Order.TTheory GRing.Theory Num.Theory.
 
 Local Open Scope ring_scope.
diff --git a/theories/landau.v b/theories/landau.v
index d2b508459..dd43504cd 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -92,10 +92,12 @@ Require Import prodnormedzmodule.
 (*          "=O_(x \near F)", not in the syntax "=O_(x : U)".                 *)
 (*                                                                            *)
 (******************************************************************************)
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
+
+Declare Scope R_scope.
+
 Import Order.TTheory GRing.Theory Num.Theory.
 
 Reserved Notation "{o_ F f }" (at level 0, F at level 0, format "{o_ F  f }").
diff --git a/theories/normedtype.v b/theories/normedtype.v
index de1504ff7..82624f860 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -2119,25 +2119,6 @@ End at_left_right.
 
 Typeclasses Opaque at_left at_right.
 
-
-Section TODO_add_to_ssrnum.
-
-Lemma maxr_real (K : realDomainType) (x y : K) :
-  x \is Num.real -> y \is Num.real -> maxr x y \is Num.real.
-Proof.
-by rewrite !realE => /orP[|] x0 /orP[|] y0; rewrite le_maxr le_maxl x0 y0 !(orbT,orTb).
-Qed.
-
-Lemma bigmaxr_real (K : realDomainType) (R : choiceType) (x : K) (D : seq R) (f : R -> K):
-  x \is Num.real ->
-  (forall x, x \in D -> f x \is Num.real) ->
-  \big[maxr/x]_(n <- D) f n \is Num.real.
-Proof.
-move=> ?; elim/big_ind : _ => // *; by [rewrite maxr_real | rewrite num_real].
-Qed.
-
-End TODO_add_to_ssrnum.
-
 Section cvg_seq_bounded.
 Context {K : numFieldType}.
 Local Notation "'+oo'" := (@pinfty_nbhs K).
@@ -2856,8 +2837,8 @@ have /Aco [] := covA.
   by rewrite -{1}(subrK p q) ler_norm_add.
 move=> D _ DcovA.
 exists (\big[maxr/0]_(i : D) (fsval i)%:~R).
-rewrite bigmaxr_real ?real0 //; split => //.
-move=> x ltmaxx p /DcovA [n Dn /lt_trans /(_ _)/ltW].
+rewrite bigmax_real ?real0//; last by move=> ? _; rewrite realz.
+split => // x ltmaxx p /DcovA [n Dn /lt_trans /(_ _)/ltW].
 apply; apply: le_lt_trans ltmaxx.
 have {} : n \in enum_fset D by [].
 rewrite enum_fsetE => /mapP[/= i iD ->]; exact/BigmaxBigminr.ler_bigmaxr.
diff --git a/theories/reals.v b/theories/reals.v
index 97a62a112..d77417672 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -13,6 +13,8 @@ From mathcomp Require Import all_ssreflect all_algebra.
 
 Require Import Setoid.
 
+Declare Scope real_scope.
+
 (* -------------------------------------------------------------------- *)
 Set   Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/topology.v b/theories/topology.v
index a92f1bbf2..ccdebdd38 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2823,7 +2823,7 @@ Lemma open_hausdorff : hausdorff T =
                 [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0]).
 Proof.
 rewrite propeqE; split => [T_filterT2|T_openT2] x y.
-  have := contra_not (T_filterT2 x y); rewrite (rwP eqP) (rwP negP) => cl /cl.
+  have := contra_not _ _ (T_filterT2 x y); rewrite (rwP eqP) (rwP negP) => cl /cl.
   rewrite [cluster _ _](rwP forallp_asboolP) => /negP.
   rewrite forallbE => /existsp_asboolPn/=[A]/negP/existsp_asboolPn/=[B].
   rewrite [nbhs _ _ -> _](rwP imply_asboolP) => /negP.

From 33b2098a583c11b372bb474e735a56dc7cbcfc6f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 15 Dec 2020 10:34:55 +0900
Subject: [PATCH 5/6] remove lemmas and update INSTALL.md

- ltr_distW and ler_distW are now subsumed by MathComp lemmas
---
 INSTALL.md            | 24 ++++++++++++------------
 theories/normedtype.v | 24 +++++-------------------
 2 files changed, 17 insertions(+), 31 deletions(-)

diff --git a/INSTALL.md b/INSTALL.md
index a3945bce7..1fae81a53 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -2,9 +2,9 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.11](https://coq.inria.fr)
-- [Mathematical Components version = 1.11.0](https://github.com/math-comp/math-comp)
-- [Finmap library version ≥ 1.5.0](https://github.com/math-comp/finmap)
+- [The Coq Proof Assistant version ≥ 8.12](https://coq.inria.fr)
+- [Mathematical Components version = 1.12.0](https://github.com/math-comp/math-comp)
+- [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
 
 These requirements can be installed in a custom way, or through
 [opam](https://opam.ocaml.org/) (the recommended way) using
@@ -20,7 +20,7 @@ Detailed instructions for possible installations of Mathematical Components are
   + type `opam install coq-mathcomp-analysis.X.Y.Z` where `X.Y.Z` is the version number
     (all the dependencies should be automatically installed, assuming `opam` has been properly
     configured and `coq-released` repository is added)
-- Custom (assuming Coq ≥ 8.11, Mathematical Components version = 1.11.0, Finmap version ≥ 1.5.0,
+- Custom (assuming Coq ≥ 8.12, Mathematical Components version = 1.12.0, Finmap version ≥ 1.5.1,
   and Hierarchy Builder ≥ 0.10.0 have been installed):
   + type `make` to use the provided `Makefile`
 
@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.3.4
+$ opam install coq-mathcomp-analysis.0.3.5
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
@@ -70,7 +70,7 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
 
-With the example of Coq 8.12.0 and MathComp 1.11.0. For other versions, update the
+With the example of Coq 8.12.0 and MathComp 1.12.0. For other versions, update the
 version numbers accordingly.
 
 1. Install Coq 8.12.0
@@ -79,15 +79,15 @@ $ opam install coq.8.12.0
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.1.11.0
-$ opam install coq-mathcomp-fingroup.1.11.0
-$ opam install coq-mathcomp-algebra.1.11.0
-$ opam install coq-mathcomp-solvable.1.11.0
-$ opam install coq-mathcomp-field.1.11.0
+$ opam install coq-mathcomp-ssreflect.1.12.0
+$ opam install coq-mathcomp-fingroup.1.12.0
+$ opam install coq-mathcomp-algebra.1.12.0
+$ opam install coq-mathcomp-solvable.1.12.0
+$ opam install coq-mathcomp-field.1.12.0
 ```
 3. Install the Finite maps library
 ```
-$ opam install coq-mathcomp-finmap.1.5.0
+$ opam install coq-mathcomp-finmap.1.5.1
 ```
 4. Install the Hierarchy Builder
 ```
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 82624f860..824bc8f9b 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -81,19 +81,6 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 
 Local Open Scope ring_scope.
-
-Section add_to_mathcomp.
-
-Lemma ltr_distW (R : realDomainType) (x y e : R) :
-  `|x - y| < e -> y - e < x.
-Proof. by rewrite ltr_distl => /andP[]. Qed.
-
-Lemma ler_distW (R : realDomainType) (x y e : R):
-  `|x - y| <= e -> y - e <= x.
-Proof. by rewrite ler_distl => /andP[]. Qed.
-
-End add_to_mathcomp.
-
 Local Open Scope classical_set_scope.
 
 Lemma nbhsN (R : numFieldType) (x : R^o) :
@@ -2065,9 +2052,8 @@ have /cauchy_ballP /cauchyP /(_ 1) [//|x0 x01] := F_cauchy.
 have D_has_sup : has_sup D; first split.
 - exists (x0 - 1) => A FA.
   near F => x.
-  apply/downP; exists x.
-  by near: x.
-  by rewrite ler_distW 1?distrC 1?ltW ?andbT //; near: x.
+  apply/downP; exists x; first by near: x.
+  by rewrite ler_distl_subl // ltW //; near: x.
 - exists (x0 + 1); apply/ubP => x /(_ _ x01) /downP [y].
   rewrite -[ball _ _ _]/(_ (_ < _)) ltr_distl ltr_subl_addr => /andP[/ltW].
   by move=> /(le_trans _) yx01 _ /yx01.
@@ -2584,7 +2570,7 @@ apply: segment_connected.
   exists i => //; apply/xe_fi; rewrite /ball_/= distrC ger0_norm.
     have lezy : z <= y by rewrite (itvP ayz).
     rewrite ltr_subl_addl; apply: le_lt_trans lezy _; rewrite -ltr_subl_addr.
-    by have := xe_y; rewrite /ball_ => /ltr_distW.
+    by have := xe_y; rewrite /ball_ => /ltr_distlC_subl.
   by rewrite subr_ge0; apply/ltW.
 exists A; last by rewrite predeqE => x; split=> [[] | []].
 move=> x clAx; have abx : x \in `[a, b].
@@ -2603,7 +2589,7 @@ exists i; first by rewrite /= !inE eq_refl.
 apply/xe_fi; rewrite /ball_/= ger0_norm; last first.
   by rewrite subr_ge0 (itvP axz).
 rewrite ltr_subl_addl -ltr_subl_addr; apply: lt_trans ltyz.
-by apply: ltr_distW; rewrite distrC.
+by apply: ltr_distlC_subl; rewrite distrC.
 Qed.
 
 End segment.
@@ -2660,7 +2646,7 @@ have /fcont /(_ _ (@nbhsx_ballx _ [normedModType R of R^o] _ e)) [_/posnumP[d] s
 have atrF := at_right_proper_filter (sup A); near (at_right (sup A)) => x.
 have /supdfe /= : @ball _ [normedModType R of R^o] (sup A) d%:num x.
   by near: x; rewrite /= nbhs_simpl; exists d%:num => //.
-rewrite /= => /ltr_distW; apply: le_lt_trans.
+rewrite /= => /ltr_distlC_subl; apply: le_lt_trans.
 rewrite ler_add2r ltW //; suff : forall t, t \in `](sup A), b] -> v < f t.
   apply; rewrite inE; apply/andP; split; first by near: x; exists 1.
   near: x; exists (b - sup A) => /=.

From a5101620d684ceceacaf1293f956acaf52ef00de Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 17 Dec 2020 23:55:11 +0900
Subject: [PATCH 6/6] add changelog and fix INSTALL.md

---
 CHANGELOG_UNRELEASED.md | 15 +++++++++++++++
 INSTALL.md              |  6 +++---
 2 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c1ee5bdc8..44c38e799 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -6,10 +6,25 @@
 
 ### Changed
 
+- Requires:
+  + MathComp >= 1.12
+- in `boolp.v`:
+  + lemmas `contra_not`, `contra_notT`, `contra_notN`, `contra_not_neq`, `contraPnot`
+    are now provided by MathComp 1.12
+- in `normedtype.v`:
+  + lemmas `ltr_distW`, `ler_distW` are now provided by MathComp 1.12 as lemmas
+    `ltr_distlC_subl` and `ler_distl_subl`
+  + lemmas `maxr_real` and `bigmaxr_real` are now provided by MathComp 1.12 as
+    lemmas `max_real` and `bigmax_real`
+  + definitions `isBOpen` and `isBClosed` are replaced by the definition `bound_side`
+  + definition `Rhull` now uses `BSide` instead of `BOpen_if`
+
 ### Renamed
 
 ### Removed
 
+- Drop support for MathComp 1.11
+
 ### Infrastructure
 
 ### Misc
diff --git a/INSTALL.md b/INSTALL.md
index 1fae81a53..b16d5179b 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -2,9 +2,10 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.12](https://coq.inria.fr)
+- [The Coq Proof Assistant version ≥ 8.11](https://coq.inria.fr)
 - [Mathematical Components version = 1.12.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
+- [Hierarchy builder version >= 0.10.0](https://github.com/math-comp/hierarchy-builder)
 
 These requirements can be installed in a custom way, or through
 [opam](https://opam.ocaml.org/) (the recommended way) using
@@ -20,8 +21,7 @@ Detailed instructions for possible installations of Mathematical Components are
   + type `opam install coq-mathcomp-analysis.X.Y.Z` where `X.Y.Z` is the version number
     (all the dependencies should be automatically installed, assuming `opam` has been properly
     configured and `coq-released` repository is added)
-- Custom (assuming Coq ≥ 8.12, Mathematical Components version = 1.12.0, Finmap version ≥ 1.5.1,
-  and Hierarchy Builder ≥ 0.10.0 have been installed):
+- Custom (assuming the requirements are met):
   + type `make` to use the provided `Makefile`
 
 ## From scratch instructions