fixes #1017

math-comp · Sep 21, 2023 · 114d06c · 114d06c
1 parent 4b7b474
commit 114d06c
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -89,6 +89,9 @@
 - in `lebesgue_integral.v`:
   + implicits of `integral_le_bound`
 
+- in `measure.v`:
+  + implicits of `measurable_fst` and `measurable_snd`
+
 ### Renamed
 
 - in `normedtype.v`: 

diff --git a/theories/measure.v b/theories/measure.v
@@ -4311,6 +4311,8 @@ Lemma measurable_swap : measurable_fun [set: _] (@swap T1 T2).
 Proof. exact: measurable_fun_prod. Qed.
 
 End prod_measurable_proj.
+Arguments measurable_fst {d1 d2 T1 T2}.
+Arguments measurable_snd {d1 d2 T1 T2}.
 #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_fst`")]
 Notation measurable_fun_fst := measurable_fst.
 #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_snd`")]