diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v
index 99dbb9f7b4..6447db2ec3 100644
--- a/theories/probability_theory/random_variable.v
+++ b/theories/probability_theory/random_variable.v
@@ -19,32 +19,54 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral hoelder.
 (* of `Lfun P n` hypotheses instead of the `integrable` predicate from        *)
 (* `lebesgue_integral.v`.                                                     *)
 (*                                                                            *)
-(* ```                                                                        *)
-(*      {RV P >-> T'} == random variable: a measurable function to the        *)
-(*                       measurableType T' from the measured space            *)
-(*                       characterized by the probability P                   *)
-(*   distribution P X == measure image of the probability measure P by the    *)
-(*                       random variable X : {RV P -> T'}                     *)
-(*                       P as type probability T R with T of type             *)
-(*                       measurableType.                                      *)
-(*                       Declared as an instance of probability measure.      *)
-(*            'E_P[X] == expectation of the real measurable function X        *)
-(*     covariance X Y == covariance between real random variable X and Y      *)
-(*            'V_P[X] == variance of the real random variable X               *)
-(*             'M_P X == moment generating function of the random variable X  *)
-(*                       with sample space corresponding to the probability   *)
-(*                       measure P                                            *)
-(*    {dmfun T >-> R} == type of discrete real-valued measurable functions    *)
-(*      {dRV P >-> R} == real-valued discrete random variable                 *)
-(*          dRV_dom X == domain of the discrete random variable X             *)
-(*         dRV_enum X == bijection between the domain and the range of X      *)
-(*            pmf X r := fine (P (X @^-1` [set r]))                           *)
-(*            cdf X r == cumulative distribution function of X                *)
-(*                    := distribution P X `]-oo, r]                           *)
-(*           ccdf X r == complementary cumulative distribution function of X  *)
-(*                    := distribution P X `]r, +oo[                           *)
-(*      enum_prob X k == probability of the kth value in the range of X       *)
-(* ```                                                                        *)
+(* `{RV P >-> T'}`                                                            *)
+(*     ~ random variable: a measurable function to the `measurableType T'`    *)
+(*       from the measured space characterized by the probability `P`         *)
+(*                                                                            *)
+(* `distribution P X`                                                         *)
+(*     ~ measure image of the probability measure `P` by the random variable  *)
+(*       `X : {RV P -> T'}`                                                   *)
+(*     ~ `P` has type `probability T R` with `T` of type `measurableType`.    *)
+(*     ~ Declared as an instance of probability measure.                      *)
+(*                                                                            *)
+(* `'E_P[X]`                                                                  *)
+(*     ~ expectation of the real measurable function `X`                      *)
+(*                                                                            *)
+(* `covariance X Y`                                                           *)
+(*     ~ covariance between real random variable `X` and `Y`                  *)
+(*                                                                            *)
+(* `'V_P[X]`                                                                  *)
+(*     ~ variance of the real random variable `X`                             *)
+(*                                                                            *)
+(* `'M_P X`                                                                   *)
+(*     ~ moment generating function of the random variable `X` with sample    *)
+(*       space corresponding to the probability measure `P`                   *)
+(*                                                                            *)
+(* `{dmfun T >-> R}`                                                          *)
+(*     ~ type of discrete real-valued measurable functions                    *)
+(*                                                                            *)
+(* `{dRV P >-> R}`                                                            *)
+(*     ~ real-valued discrete random variable                                 *)
+(*                                                                            *)
+(* `dRV_dom X`                                                                *)
+(*     ~ domain of the discrete random variable `X`                           *)
+(*                                                                            *)
+(* `dRV_enum X`                                                               *)
+(*     ~ bijection between the domain and the range of `X`                    *)
+(*                                                                            *)
+(* `pmf X r`                                                                  *)
+(*     ~ ``fine (P (X @^-1` [set r]))``                                       *)
+(*                                                                            *)
+(* `cdf X r`                                                                  *)
+(*     ~ cumulative distribution function of `X`                              *)
+(*     ~ ``:= distribution P X `]-oo, r]``                                    *)
+(*                                                                            *)
+(* `ccdf X r`                                                                 *)
+(*     ~ complementary cumulative distribution function of `X`                *)
+(*     ~ := ``distribution P X `]r, +oo[``                                    *)
+(*                                                                            *)
+(* `enum_prob X k`                                                            *)
+(*     ~ probability of the kth value in the range of `X`                     *)
 (*                                                                            *)
 (*                                                                            *)
 (******************************************************************************)