diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
index 8be92cff29..436ff5872f 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
@@ -26,11 +26,11 @@ From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable.
 (* Detailed contents:                                                         *)
 (* ```                                                                        *)
 (*               m1 \x m2 == product measure over T1 * T2, m1 is a measure    *)
-(*                           measure over T1, and m2 is a sigma finite        *)
-(*                           measure over T2                                  *)
+(*                           over T1, and m2 is a sigma finite measure over   *)
+(*                           T2                                               *)
 (*              m1 \x^ m2 == product measure over T1 * T2, m2 is a measure    *)
-(*                           measure over T1, and m1 is a sigma finite        *)
-(*                           measure over T2                                  *)
+(*                           over T1, and m1 is a sigma finite measure over   *)
+(*                           T2                                               *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)