Merge pull request #135 from math-comp/test_with_mathcomp-1.8.0

Porting to mathcomp-1.8.0

.travis.yml

@@ -14,9 +14,9 @@ env:
   - NJOBS="2"
   - CONTRIB_NAME="analysis"
   matrix:
-  - DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-8.8"
-  - DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-8.9"
-  - DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-dev"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.8"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.9"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-dev"
 
 install: |
   # Prepare the COQ container

Rstruct.v

@@ -132,7 +132,7 @@ by rewrite Rmult_0_r eq_sym R1_neq_0.
 Qed.
 
 Lemma Rinvx_out : {in predC unit_R, Rinvx =1 id}.
-Proof. by move=> x; rewrite inE /= /Rinvx -if_neg => ->. Qed.
+Proof. by move=> x; rewrite inE/= /Rinvx -if_neg => ->. Qed.
 
 Definition R_unitRingMixin :=
   UnitRingMixin RmultRinvx RinvxRmult intro_unit_R Rinvx_out.
@@ -599,7 +599,8 @@ Lemma bmaxrf_index n (f : {ffun 'I_n.+1 -> R}) :
   (index (bmaxrf f) (codom f) < n.+1)%N.
 Proof.
 rewrite /bmaxrf.
-have {6}-> : n.+1 = size (codom f) by rewrite size_codom card_ord.
+rewrite [in X in (_ < X)%N](_ : n.+1 = size (codom f)); last first.
+  by rewrite size_codom card_ord.
 by apply: bigmaxr_index; rewrite size_codom card_ord.
 Qed.
 
@@ -612,7 +613,7 @@ Lemma eq_index_bmaxrf n (f : {ffun 'I_n.+1 -> R}) :
   f (index_bmaxrf f) = bmaxrf f.
 Proof.
 move: (bmaxrf_index f).
-rewrite -{3}[n.+1]card_ord -(size_codom f) index_mem.
+rewrite -[X in _ (_ < X)%N]card_ord -(size_codom f) index_mem.
 move/(nth_index (f ord0)) => <-; rewrite (nth_map ord0).
   by rewrite (ordnat (bmaxrf_index _)) /index_bmaxrf nth_ord_enum.
 by rewrite size_enum_ord; apply: bmaxrf_index.

altreals/distr.v

@@ -795,7 +795,7 @@ Lemma dfstE (mu : {distr (T * U) /  R}) x :
 Proof.
 rewrite dmargin_psumE /=; pose h y : T * U := (x, y).
 rewrite (reindex_psum (P := [pred z | z.1 == x]) (h := h)) /=.
-+ case=> a b; rewrite !inE /= mulf_eq0 => /norP[].
++ case=> a b; rewrite !inE/= mulf_eq0 => /norP[].
   by rewrite pnatr_eq0 eqb0 negbK.
 + by exists snd => [z|[z1 z2]]; rewrite !inE //= => /eqP ->.
 by apply/eq_psum => y; rewrite eqxx mul1r.

altreals/realseq.v

@@ -123,7 +123,7 @@ case: l1 l2 => [l1||] [l2||] //= lt_l12; last first.
   by move=> lt1 lt2; apply/(ltr_trans lt1).
 pose e := l2 - l1; exists (B l1 (e/2%:R)), (B l2 (e/2%:R)).
 have gt0_e: 0 < e by rewrite subr_gt0.
-move=> x y; rewrite !inE /= /eclamp pmulr_rle0 // invr_le0.
+move=> x y; rewrite !inE/= /eclamp pmulr_rle0 // invr_le0.
 rewrite lern0 /= !ltr_distl => /andP[_ lt1] /andP[lt2 _].
 apply/(ltr_trans lt1)/(ler_lt_trans _ lt2).
 rewrite ler_subr_addl addrCA -mulrDl -mulr2n -mulr_natr.
@@ -140,7 +140,7 @@ wlog: l1 l2 / (l1 < l2)%E => [wlog ne_l12|le_l12 _].
   case/wlog=> [|x [y h]]; first by rewrite eq_sym.
   by exists y, x=> z; rewrite inE andbC /= (h z).
 case/separable_le: le_l12 => [v1] [v2] h; exists v1, v2.
-move=> x; apply/negP; rewrite inE /= => /andP[] xv1 xv2.
+move=> x; apply/negP; rewrite inE/= => /andP[] xv1 xv2.
 by have := h _ _ xv1 xv2; rewrite ltrr.
 Qed.
 
@@ -182,7 +182,7 @@ Proof.
 move=> cv1 cv2; apply/eqP; case: (l1 =P l2) => // /eqP.
 case/separable=> [n1] [n2] h; move: (cv1 n1) (cv2 n2).
 case=> [K1 c1] [K2 c2]; pose K := maxn K1 K2.
-move/(_ (u K)): h; rewrite !inE /= !(c1, c2) //.
+move/(_ (u K)): h; rewrite !inE/= !(c1, c2) //.
   by apply/leq_maxl. by apply/leq_maxr.
 Qed.
 

altreals/realsum.v

@@ -193,7 +193,7 @@ Proof.
 case/ncvg_mono=> -[x||] // _ cu bdu; first by exists x.
 case/asboolP/nboundedP: bdu=> M gt0_M bdu.
 case/(_ (NPInf M)): cu => K /= /(_ K (leqnn _)).
-rewrite inE /= => /ltrW /ler_trans /(_ (ler_norm _)).
+rewrite inE/= => /ltrW /ler_trans /(_ (ler_norm _)).
 by move/ler_lt_trans/(_ (bdu _)); rewrite ltrr.
 Qed.
 End PosCnv.
@@ -369,7 +369,7 @@ Lemma psum_fin (f : I -> R) : psum f = \sum_i `|f i|.
 Proof.                          (* FIXME *)
 pose S := \sum_(i : [fset i | i : I]) `|f (val i)|.
 rewrite /psum (asboolT (summable_fin f)) (@max_sup _ S).
-  rewrite inE /=; apply/andP; split; first apply/imsetbP.
+  rewrite inE/=; apply/andP; split; first apply/imsetbP.
     by exists [fset i | i : I]%fset.
   apply/ubP=> y /imsetbP[J ->]; apply/(big_fset_subset (F := \`|_|)).
     by move=> i; rewrite normr_ge0.

classical_sets.v

@@ -425,8 +425,8 @@ Local Coercion base : class_of >-> Choice.class_of.
 Definition pack m :=
   fun bT b of phant_id (Choice.class bT) b => @Pack T (Class b m) T.
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
 
 End ClassDef.
 

derive.v

@@ -1290,7 +1290,7 @@ Proof.
 move=> leab fcont; set imf := [pred t | t \in f @` [set x | x \in `[a, b]]].
 have imf_sup : has_sup imf.
   apply/has_supP; split.
-    by exists (f a); rewrite !inE; apply/asboolP/imageP; rewrite inE lerr.
+    by exists (f a); rewrite !inE; apply/asboolP/imageP; rewrite inE/= lerr.
   have [M imfltM] : bounded (f @` [set x | x \in `[a, b]] : set R^o).
     apply/compact_bounded/continuous_compact; last exact: segment_compact.
     by move=> ?; rewrite inE => /asboolP /fcont.
@@ -1415,7 +1415,7 @@ apply/eqP; rewrite eqr_le; apply/andP; split.
   rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
   exists (b - c); first by rewrite subr_gt0 (itvP cab).
   move=> h; rewrite /AbsRing_ball /= absrB subr0 absRE.
-  move=> /(ler_lt_trans (ler_norm _)); rewrite ltr_subr_addr inE => ->.
+  move=> /(ler_lt_trans (ler_norm _)); rewrite ltr_subr_addr inE/= => ->.
   by move=> /ltr_spsaddl -> //; rewrite (itvP cab).
 rewrite ['D_1 f c]cvg_at_leftE; last exact: fdrvbl.
 apply: le0r_flim_map; last first.
@@ -1428,7 +1428,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 /AbsRing_ball /= absrB subr0 absRE.
-move=> /ltr_normlP []; rewrite ltr_subr_addl ltr_subl_addl inE => -> _.
+move=> /ltr_normlP []; rewrite ltr_subr_addl ltr_subl_addl inE/= => -> _.
 by move=> /ltr_snsaddl -> //; rewrite (itvP cab).
 Grab Existential Variables. all: end_near. Qed.
 
@@ -1455,24 +1455,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} cmaxab : cmax \in `]a, b[.
-    by rewrite inE !ltr_def !(itvP cmaxab) cnea eq_sym cneb.
+    by rewrite inE/= !ltr_def !(itvP cmaxab) cnea eq_sym cneb.
   exists cmax => //; apply: derive1_at_max (ltrW ltab) fdrvbl cmaxab _ => t tab.
-  by apply: fcmax; rewrite inE !ltrW // (itvP tab).
+  by apply: fcmax; rewrite inE/= !ltrW // (itvP tab).
 have [cmin cminab fcmin] := EVT_min (ltrW 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} cminab : cmin \in `]a, b[.
-    by rewrite inE !ltr_def !(itvP cminab) cnea eq_sym cneb.
+    by rewrite inE/= !ltr_def !(itvP cminab) cnea eq_sym cneb.
   exists cmin => //; apply: derive1_at_min (ltrW ltab) fdrvbl cminab _ => t tab.
-  by apply: fcmin; rewrite inE !ltrW // (itvP tab).
+  by apply: fcmin; rewrite inE/= !ltrW // (itvP tab).
 have midab : (a + b) / 2 \in `]a, b[ by apply: mid_in_itvoo.
 exists ((a + b) / 2) => //; apply: derive1_at_max (ltrW 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 eqr_le fcmax; last by rewrite inE !ltrW ?(itvP sab).
-suff -> : f cmax = f cmin by rewrite fcmin // inE !ltrW ?(itvP sab).
+apply/eqP; rewrite eqr_le fcmax; last by rewrite inE/= !ltrW ?(itvP sab).
+suff -> : f cmax = f cmin by rewrite fcmin // inE/= !ltrW ?(itvP sab).
 by case: cmaxeaVb => ->; case: cmineaVb => ->.
 Qed.
 
@@ -1482,7 +1482,7 @@ Lemma MVT (f df : R^o -> R^o) (a b : R) :
   exists2 c, c \in `[a, b] & f b - f a = df c * (b - a).
 Proof.
 move=> leab fdrvbl fcont; move: leab; rewrite ler_eqVlt => /orP [/eqP aeb|altb].
-  by exists a; [rewrite inE aeb lerr|rewrite aeb !subrr mulr0].
+  by exists a; [rewrite inE/= aeb lerr|rewrite aeb !subrr mulr0].
 set g := f + (- ( *:%R^~ ((f b - f a) / (b - a)) : R -> R)).
 have gdrvbl : forall x, x \in `]a, b[ -> derivable g x 1.
   by move=> x /fdrvbl dfx; apply: derivableB => //; apply/derivable1_diffP.

normedtype.v

@@ -98,7 +98,7 @@ Section ClassDef.
 
 Record class_of (K : Type) := Class {
   base : Num.NumDomain.class_of K ;
-  mixin : mixin_of (Num.NumDomain.Pack base K)
+  mixin : mixin_of (Num.NumDomain.Pack base)
 }.
 Local Coercion base : class_of >-> Num.NumDomain.class_of.
 Local Coercion mixin : class_of >-> mixin_of.
@@ -111,19 +111,19 @@ Definition class := let: Pack _ c _ := cT return class_of cT in c.
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 Definition clone c of phant_id class c := @Pack T c T.
-Definition pack b0 (m0 : mixin_of (@Num.NumDomain.Pack T b0 T)) :=
+Definition pack b0 (m0 : mixin_of (@Num.NumDomain.Pack T b0)) :=
   fun bT b & phant_id (Num.NumDomain.class bT) b =>
   fun    m & phant_id m0 m => Pack (@Class T b m) T.
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition ringType := @GRing.Ring.Pack cT xclass xT.
-Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
-Definition numDomainType := @Num.NumDomain.Pack cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition ringType := @GRing.Ring.Pack cT xclass.
+Definition comRingType := @GRing.ComRing.Pack cT xclass.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
+Definition numDomainType := @Num.NumDomain.Pack cT xclass.
 
 End ClassDef.
 
@@ -393,10 +393,10 @@ Lemma in_segment_addgt0Pr (R : realFieldType) (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).
+  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.
+rewrite inE/=; apply/andP.
+by split; apply/ler_addgt0Pr => ? /xyz_e /andP /= []; rewrite ler_subl_addr.
 Qed.
 
 Lemma in_segment_addgt0Pl (R : realFieldType) (x y z : R) :
@@ -411,8 +411,8 @@ Proof. by []. Qed.
 
 Lemma Rhausdorff : hausdorff [topologicalType of R].
 Proof.
-move=> x y clxy.
-apply/eqP; rewrite eqr_le; apply/in_segment_addgt0Pr => _ /posnumP[e].
+move=> x y clxy; apply/eqP; rewrite eqr_le.
+apply/(@in_segment_addgt0Pr _ x _ x) => _ /posnumP[e].
 rewrite inE -ler_distl -absRE; set he := (e%:num / 2)%:pos.
 have [z []] := clxy _ _ (locally_ball x he) (locally_ball y he).
 rewrite ball_absE /ball_ absrB => zx_he yz_he.
@@ -525,7 +525,7 @@ Record class_of (T : Type) := Class {
   locally_mixin : Filtered.locally_of T T ;
   topological_mixin : @Topological.mixin_of T locally_mixin ;
   uniform_mixin : @Uniform.mixin_of T locally_mixin;
-  mixin : @mixin_of _ (@GRing.Lmodule.Pack K (Phant K) T base T) _ uniform_mixin
+  mixin : @mixin_of _ (@GRing.Lmodule.Pack K (Phant K) T base) _ uniform_mixin
 }.
 Local Coercion base : class_of >-> GRing.Lmodule.class_of.
 Definition base2 T (c : class_of T) :=
@@ -550,21 +550,21 @@ Definition clone c of phant_id class c := @Pack phK T c T.
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition pack b0 l0 um0 (m0 : @mixin_of _ (@GRing.Lmodule.Pack K (Phant K) T b0 T) l0 um0) :=
+Definition pack b0 l0 um0 (m0 : @mixin_of _ (@GRing.Lmodule.Pack K (Phant K) T b0) l0 um0) :=
   fun bT b & phant_id (@GRing.Lmodule.class K phK bT) b =>
   fun ubT (ub : Uniform.class_of _) & phant_id (@Uniform.class ubT) ub =>
   fun   m & phant_id m0 m => Pack phK (@Class T b ub ub ub ub m) T.
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition lmodType := @GRing.Lmodule.Pack K phK cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition lmodType := @GRing.Lmodule.Pack K phK cT xclass.
 Definition pointedType := @Pointed.Pack cT xclass xT.
 Definition filteredType := @Filtered.Pack cT cT xclass xT.
 Definition topologicalType := @Topological.Pack cT xclass xT.
 Definition uniformType := @Uniform.Pack cT xclass xT.
-Definition join_zmodType := @GRing.Zmodule.Pack uniformType xclass xT.
-Definition join_lmodType := @GRing.Lmodule.Pack K phK uniformType xclass xT.
+Definition join_zmodType := @GRing.Zmodule.Pack uniformType xclass.
+Definition join_lmodType := @GRing.Lmodule.Pack K phK uniformType xclass.
 End ClassDef.
 
 Module Exports.
@@ -1167,17 +1167,17 @@ Definition pack :=
 Let xT := let: Pack T _ _ := cT in T.
 Notation xclass := (class : class_of xT).
 
-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition lmodType := @GRing.Lmodule.Pack K phK cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass.
+Definition lmodType := @GRing.Lmodule.Pack K phK cT xclass.
 Definition pointedType := @Pointed.Pack cT xclass xT.
 Definition filteredType := @Filtered.Pack cT cT xclass xT.
 Definition topologicalType := @Topological.Pack cT xclass xT.
 Definition uniformType := @Uniform.Pack cT xclass xT.
 Definition completeType := @Complete.Pack cT xclass xT.
-Definition join_zmodType := @GRing.Zmodule.Pack completeType xclass xT.
-Definition join_lmodType := @GRing.Lmodule.Pack K phK completeType xclass xT.
+Definition join_zmodType := @GRing.Zmodule.Pack completeType xclass.
+Definition join_lmodType := @GRing.Lmodule.Pack K phK completeType xclass.
 Definition normedModType := @NormedModule.Pack K phK cT xclass xT.
 Definition join_completeType := @Complete.Pack normedModType xclass xT.
 End ClassDef.
@@ -1532,9 +1532,9 @@ set B := [set x | exists2 D' : {fset I}, {subset D' <= D} &
 set A := [set x | x \in `[a, b]] `&` B.
 suff Aeab : A = [set x | x \in `[a, b]].
   suff [_ [D' ? []]] : A b by exists D'.
-  by rewrite Aeab inE; apply/andP.
+  by rewrite Aeab inE/=; apply/andP.
 apply: segment_connected.
-- have aba : a \in `[a, b] by rewrite inE; apply/andP.
+- have aba : a \in `[a, b] by rewrite inE/=; apply/andP.
   exists a; split=> //; have /sabUf [i Di fia] := aba.
   exists [fset i]%fset; first by move=> ?; rewrite inE in_setE => /eqP->.
   split; last by exists i => //; rewrite inE.
@@ -1545,7 +1545,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 inE/= (itvP ayz) lezx.
   exists i=> //; apply/xe_fi; rewrite /AbsRing_ball/ball_ absrB absRE ger0_norm.
     have lezy : z <= y by rewrite (itvP ayz).
     rewrite ltr_subl_addl; apply: ler_lt_trans lezy _; rewrite -ltr_subl_addr.
@@ -1562,7 +1562,7 @@ split=> [z axz|]; last first.
   exists i; first by rewrite !inE eq_refl.
   exact/xe_fi/(@ball_center [uniformType of R]).
 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 inE/= (itvP axz) lezy.
   by exists j => //; rewrite inE orbC Dj.
 exists i; first by rewrite !inE eq_refl.
 apply/xe_fi; rewrite /AbsRing_ball/ball_ absRE ger0_norm; last first.
@@ -1596,9 +1596,9 @@ move=> leab; wlog : f v / f a <= f b.
   by move=> c cab /eqP; rewrite eqr_opp => /eqP; exists c.
 move=> lefab fcont; rewrite minr_l // maxr_r // => /andP [].
 rewrite ler_eqVlt => /orP [/eqP<- _|ltfav].
-  by exists a => //; rewrite inE lerr leab.
+  by exists a => //; rewrite inE/= lerr leab.
 rewrite ler_eqVlt => /orP [/eqP->|ltvfb].
-  by exists b => //; rewrite inE lerr leab.
+  by exists b => //; rewrite inE/= lerr leab.
 set A := [pred c | (c <= b) && (f c <= v)].
 have An0 : reals.nonempty A by exists a; apply/andP; split=> //; apply: ltrW.
 have supA : has_sup A.
@@ -1634,9 +1634,9 @@ rewrite ler_add2r ltrW //; suff : forall t, t \in `](sup A), b] -> v < f t.
     by move: lefsupv; rewrite lerNgt -besup ltvfb.
   move=> t lttb ltsupt; move: lttb; rewrite /AbsRing_ball /= absrB absRE.
   by rewrite gtr0_norm ?subr_gt0 // ltr_add2r; apply: ltrW.
-move=> t /andP [ltsupt letb]; rewrite ltrNge; apply/negP => leftv.
-move: ltsupt; rewrite ltrNge => /negP; apply; apply: sup_upper_bound => //.
-by rewrite inE letb leftv.
+move=> t /andP [ltsupt /= letb]; rewrite ltrNge; apply/negP => leftv.
+move: ltsupt => /=; rewrite ltrNge => /negP; apply; apply: sup_upper_bound => //.
+by rewrite inE leftv letb.
 Grab Existential Variables. all: end_near. Qed.
 
 (** Local properties in [R] *)

opam

@@ -1,8 +1,8 @@
-opam-version: "1.2"
+opam-version: "2.0"
 maintainer: "[email protected]"
 homepage: "https://github.com/math-comp/analysis"
 bug-reports: "https://github.com/math-comp/analysis/issues"
-dev-repo: "https://github.com/math-comp/analysis.git"
+dev-repo: "git+https://github.com/math-comp/analysis.git"
 license: "CeCILL-C"
 authors: [
   "Reynald Affeldt"
@@ -21,8 +21,14 @@ install: [
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/mathcomp/analysis"]
 depends: [
   "coq" { (>= "8.8" | = "dev") }
-  "coq-mathcomp-field"       {(>= "1.7.0" & < "1.8.0~")}
+  "coq-mathcomp-field"       {(>= "1.8.0" & < "1.9.0~")}
   "coq-mathcomp-bigenough"   {(>= "1.0.0" & < "1.1.0~")}
-  "coq-mathcomp-finmap"      {(>= "1.1.0" & < "1.2.0~")}
+  "coq-mathcomp-finmap"      {(>= "1.2.0" & < "1.3.0~")}
 ]
 synopsis: "An analysis library for mathematical components"
+description: """
+This repository contains an experimental library for real analysis for
+the Coq proof-assistant and using the Mathematical Components library.
+
+It is inspired by the Coquelicot library.
+"""