Adapt to math-comp/math-comp#1131

theories/kernel.v

@@ -849,16 +849,14 @@ Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
 Variable l : R.-ker X ~> Y.
 Variable k : R.-ker [the measurableType _ of X * Y] ~> Z.
 
-Local Notation "l \; k" := (kcomp l k).
-
-Let kcomp0 x : (l \; k) x set0 = 0.
+Let kcomp0 x : kcomp l k x set0 = 0.
 Proof.
 by rewrite /kcomp (eq_integral (cst 0)) ?integral0// => y _; rewrite measure0.
 Qed.
 
-Let kcomp_ge0 x U : 0 <= (l \; k) x U. Proof. exact: integral_ge0. Qed.
+Let kcomp_ge0 x U : 0 <= kcomp l k x U. Proof. exact: integral_ge0. Qed.
 
-Let kcomp_sigma_additive x : semi_sigma_additive ((l \; k) x).
+Let kcomp_sigma_additive x : semi_sigma_additive (kcomp l k x).
 Proof.
 move=> U mU tU mUU; rewrite [X in _ --> X](_ : _ =
   \int[l x]_y (\sum_(n <oo) k (x, y) (U n))); last first.
@@ -871,10 +869,10 @@ exact: measurableT_comp (measurable_kernel k _ (mU n)) _.
 Qed.
 
 HB.instance Definition _ x := isMeasure.Build _ _ R
-  ((l \; k) x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x).
+  (kcomp l k x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x).
 
 Definition mkcomp : X -> {measure set Z -> \bar R} := fun x =>
-  [the measure _ _ of (l \; k) x].
+  [the measure _ _ of kcomp l k x].
 
 End kcomp_is_measure.