adding Import numFieldNormedType.Exports. solve the ^o problem

theories/charge.v

@@ -92,6 +92,7 @@ Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope ring_scope.
 Local Open Scope classical_set_scope.
@@ -700,7 +701,7 @@ have nuAoo : 0 <= nu Aoo.
 have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0.
   rewrite [X in X @ _ --> _](_ : _ = (fun n => (fine (nu (A_ (v n))))%:E)); last first.
     by apply/funext => n/=; rewrite fineK// fin_num_measure.
-  apply: continuous_cvg => //; apply: (@cvg_series_cvg_0 _ R^o).
+  apply: continuous_cvg => //; apply: cvg_series_cvg_0.
   rewrite (_ : series _ = fine \o (fun n => \sum_(0 <= i < n) nu (A_ (v i)))); last first.
     apply/funext => n /=.
     by rewrite /series/= sum_fine//= => i _; rewrite fin_num_measure.
@@ -831,7 +832,7 @@ have znuD n : z_ (v n) <= nu D.
 have max_le0 n : maxe (z_ (v n) * 2^-1%:E) (- 1%E) <= 0.
   by rewrite ge_max leeN10 andbT pmule_lle0.
 have not_s_cvg_0 : ~ (z_ \o v) n @[n --> \oo]  --> 0.
-  move/fine_cvgP => -[zfin] /(@cvgrPdist_lt _ R^o).
+  move/fine_cvgP => -[zfin] /cvgrPdist_lt.
   have /[swap] /[apply] -[M _ hM] : (0 < `|fine (nu D)|)%R.
     by rewrite normr_gt0// fine_eq0// ?lt_eqF// fin_num_measure.
   near \oo => n.
@@ -862,7 +863,7 @@ have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n -->
   apply/funext => n/=; rewrite sum_fine// => m _.
   rewrite le0_fin_numE; first by rewrite lt_max ltNyr orbT.
   by rewrite /maxe; case: ifPn => // _; rewrite mule_le0_ge0.
-move/(@cvg_series_cvg_0 _ R^o) => maxe_cvg_0.
+move/cvg_series_cvg_0 => maxe_cvg_0.
 apply: not_s_cvg_0.
 rewrite (_ : _ \o _ = (fun n => z_ (v n) * 2^-1%:E) \* cst 2%:E); last first.
   by apply/funext => n/=; rewrite -muleA -EFinM mulVr ?mule1// unitfE.
@@ -874,7 +875,7 @@ apply/fine_cvgP; split.
   rewrite sub0r normrN ltNge => maxe_lt1; rewrite fin_numE; apply/andP; split.
     by apply: contra maxe_lt1 => /eqP ->; rewrite max_r ?leNye//= normrN1 lexx.
   by rewrite lt_eqF// (@le_lt_trans _ _ 0)// mule_le0_ge0.
-apply/(@cvgrPdist_lt _ R^o) => _ /posnumP[e].
+apply/cvgrPdist_lt => _ /posnumP[e].
 have : (0 < minr e%:num 1)%R by rewrite lt_min// ltr01 andbT.
 move/cvgrPdist_lt : maxe_cvg_0 => /[apply] -[M _ hM].
 near=> n; rewrite sub0r normrN.

theories/ftc.v

@@ -251,15 +251,15 @@ apply: filterS; first exact: (ae_filter_ringOfSetsType mu).
 by move=> r /=; apply; rewrite ltNyr.
 Qed.
 
-Let itv_continuous_lebesgue_pt f a (x : R) (u : R) : (x < u)%R ->
+Let itv_continuous_lebesgue_pt f a x (u : R) : (x < u)%R ->
   measurable_fun [set` Interval a (BRight u)] f ->
   a < BRight x ->
   {for x, continuous f} -> lebesgue_pt f x.
 Proof.
 move=> xu fi + fx.
 move: a fi => [b a fi /[1!(@lte_fin R)] ax|[|//] fi _].
 - near (0%R:R)^'+ => e; apply: (@continuous_lebesgue_pt _ _ _ (ball x e)) => //.
-  + exact: (ball_open_nbhs x).
+  + exact: ball_open_nbhs.
   + exact: measurable_ball.
   + apply: measurable_funS fi => //; rewrite ball_itv.
     apply: (@subset_trans _ `](x - e)%R, u]) => //.
@@ -501,7 +501,7 @@ Corollary continuous_FTC2 f F a b : (a < b)%R ->
 Proof.
 move=> ab cf dF F'f.
 pose fab := f \_ `[a, b].
-pose G x:= (\int[mu]_(t in `[a, x]) fab t)%R.
+pose G x := (\int[mu]_(t in `[a, x]) fab t)%R.
 have iabf : mu.-integrable `[a, b] (EFin \o f).
   by apply: continuous_compact_integrable => //; exact: segment_compact.
 have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable G x 1}.
@@ -615,7 +615,7 @@ Lemma integration_by_parts F G f g a b : (a < b)%R ->
 Proof.
 move=> ab cf Fab Ff cg Gab Gg.
 have cfg : {within `[a, b], continuous (f * G + F * g)%R}.
-apply/subspace_continuousP => x abx; apply:cvgD .
+apply/subspace_continuousP => x abx; apply: cvgD.
   - apply: cvgM.
     + by move/subspace_continuousP : cf; exact.
     + have := derivable_oo_continuous_bnd_within Gab.

theories/lebesgue_integral.v

@@ -1672,7 +1672,7 @@ Qed.
 End approximation_sfun.
 
 Section lusin.
-Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff ) : core.
+Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff) : core.
 Local Open Scope ereal_scope.
 Context (rT : realType) (A : set rT).
 Let mu := [the measure _ _ of @lebesgue_measure rT].
@@ -5755,7 +5755,7 @@ have ritv r : 0 < r -> mu `[x - r, x + r]%classic = (r *+ 2)%:E.
   rewrite ler_ltD // ?rE // -EFinD; congr (_ _).
   by rewrite opprB addrAC [_ - _]addrC addrA subrr add0r.
 move=> oA intf ctsfx Ax.
-apply: (@cvg_zero _ R^o).
+apply: cvg_zero.
 apply/cvgrPdist_le => eps epos; apply: filter_app (@nbhs_right_gt rT 0).
 move/cvgrPdist_le/(_ eps epos)/at_right_in_segment : ctsfx; apply: filter_app.
 apply: filter_app (open_itvcc_subset oA Ax).
@@ -6119,7 +6119,7 @@ have {}Kcmf : K `<=` cover [set i | HL f i > c%:E] (fun i => ball i (r_ i)).
 have {Kcmf}[D Dsub Kcover] : finite_subset_cover [set i | c%:E < HL f i]
     (fun i => ball i (r_ i)) K.
   move: cK; rewrite compact_cover => /(_ _ _ _ _ Kcmf); apply.
-  by move=> /= x cMfx; exact/(@ball_open _ R^o)/r_pos.
+  by move=> /= x cMfx; exact/ball_open/r_pos.
 have KDB : K `<=` cover [set` D] B.
   by apply: (subset_trans Kcover) => /= x [r Dr] rx; exists r.
 have is_ballB i : is_ball (B i) by exact: is_ball_ball.