From bd6f626ab18750420780612dee8e12880a1a809f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 22 Oct 2024 19:13:47 +0900
Subject: [PATCH 1/2] fixes #1358, fixes #1359

---
 theories/forms.v             | 2 +-
 theories/lebesgue_integral.v | 4 ++--
 theories/probability.v       | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/forms.v b/theories/forms.v
index 7c272eb06..7b7f2f732 100644
--- a/theories/forms.v
+++ b/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).
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 1c7b7ced6..7700edfee 100644
--- a/theories/lebesgue_integral.v
+++ b/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.
diff --git a/theories/probability.v b/theories/probability.v
index 29ccb0473..2fbeeb171 100644
--- a/theories/probability.v
+++ b/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.

From 8d3c8d2a0a720f7fcfee7ad9bc74ca827279898e Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 22 Oct 2024 19:16:03 +0900
Subject: [PATCH 2/2] changelog

---
 CHANGELOG_UNRELEASED.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 856cacdca..e7b54b9d8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/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