fixes #1358, fixes #1359 (#1362)

* fixes #1358, fixes #1359

CHANGELOG_UNRELEASED.md

@@ -41,6 +41,11 @@
     `sup_ent_nbhs` are now `Local`
 
 - The function `map_pair` was moved from `topology.v` to `mathcomp_extra.v`.
+- in `forms.v`:
+  + notation `'e_`
+
+- in `lebesgue_integral.v`:
+  + notation `\x`
 
 ### Renamed
 

theories/forms.v

@@ -29,7 +29,7 @@ Reserved Notation "eps_theta .-sesqui" (at level 2, format "eps_theta .-sesqui")
 
 Notation "u '``_' i" := (u (0 : 'I_1) i) : ring_scope.
 Notation "''e_' i" := (delta_mx 0 i)
- (format "''e_' i", at level 3) : ring_scope.
+  (at level 8, i at level 2, format "''e_' i") : ring_scope.
 
 Local Notation "M ^ phi" := (map_mx phi M).
 Local Notation "M ^t phi" := (map_mx phi (M ^T)) (phi at level 30, at level 30).

theories/lebesgue_integral.v

@@ -95,8 +95,8 @@ Reserved Notation "\int [ mu ]_ i F"
   (at level 36, F at level 36, mu at level 10, i at level 0,
     right associativity, format "'[' \int [ mu ]_ i '/  '  F ']'").
 Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").
-Reserved Notation "m1 '\x' m2" (at level 40, m2 at next level).
-Reserved Notation "m1 '\x^' m2" (at level 40, m2 at next level).
+Reserved Notation "m1 '\x' m2" (at level 40, left associativity).
+Reserved Notation "m1 '\x^' m2" (at level 40, left associativity).
 
 #[global]
 Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core.

theories/probability.v

@@ -134,7 +134,7 @@ End transfer_probability.
 HB.lock Definition expectation {d} {T : measurableType d} {R : realType}
   (P : probability T R) (X : T -> R) := (\int[P]_w (X w)%:E)%E.
 Canonical expectation_unlockable := Unlockable expectation.unlock.
-Arguments expectation {d T R} P _%R.
+Arguments expectation {d T R} P _%_R.
 Notation "''E_' P [ X ]" := (@expectation _ _ _ P X) : ereal_scope.
 
 Section expectation_lemmas.
@@ -213,7 +213,7 @@ HB.lock Definition covariance {d} {T : measurableType d} {R : realType}
     (P : probability T R) (X Y : T -> R) :=
   'E_P[(X \- cst (fine 'E_P[X])) * (Y \- cst (fine 'E_P[Y]))]%E.
 Canonical covariance_unlockable := Unlockable covariance.unlock.
-Arguments covariance {d T R} P _%R _%R.
+Arguments covariance {d T R} P _%_R _%_R.
 
 Section covariance_lemmas.
 Local Open Scope ereal_scope.