diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4b30c26a0..0d911f46c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -13,6 +13,9 @@
 - in set_interval.v
   + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
 
+- in `lebesgue_Rintegrable.v`:
+  + lemma `Rintegral_cst` (does not use `cst` anymore)
+
 ### Renamed
 - in set_interval.v
   + `itv_is_ray` -> `itv_is_open_unbounded`
diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index 916c0358a..5f0fe74e9 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -146,7 +146,7 @@ Lemma Rintegral_set0 f : \int[mu]_(x in set0) f x = 0.
 Proof. by rewrite /Rintegral integral_set0. Qed.
 
 Lemma Rintegral_cst D : d.-measurable D ->
-  forall r, \int[mu]_(x in D) (cst r) x = r * fine (mu D).
+  forall r, \int[mu]_(_ in D) r = r * fine (mu D).
 Proof.
 move=> mD r; rewrite /Rintegral/= integral_cst//.
 have := leey (mu D); rewrite le_eqVlt => /predU1P[->/=|muy]; last first.