diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 32ff69b16..4168b66fa 100644
--- 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
index 5fff3bb6e..49610304f 100644
--- 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`")]