diff --git a/Makefile.common b/Makefile.common
index cf974a9017..360f0162c2 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -138,15 +138,14 @@ coq2html:
 	gsed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.dot
 	gsed -i 's/\//\./g' depend.dot
 	../coq2html/tools/generate-hierarchy-graph.sh
-	../coq2html/coq2html \
+	find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs ../coq2html/coq2html \
   -hierarchy-graph hierarchy-graph.dot \
   -dependency-graph depend.dot \
   -title "Mathcomp Analysis" \
   -d html/ -base mathcomp -Q theories analysis \
   -coqlib https://coq.inria.fr/doc/V8.19.2/stdlib/ \
   -external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect \
-  -external https://math-comp.github.io/htmldoc/ mathcomp.algebra \
-  $(find . -not -path '*/.*' -name "*.v" -or -name "*.glob")
+  -external https://math-comp.github.io/htmldoc/ mathcomp.algebra
 
 coq2html-clean:
 	rm -f */*.glob
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 86b9b0ebee..8514345584 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -34,7 +34,7 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (*   set (i.e., of type set rT)                                               *)
 (* - indexed sets are rather named F                                          *)
 (*                                                                            *)
-(* Example of notations:                                                      *)
+(* Examples of notations:                                                     *)
 (* | Coq notations                |   | Meaning                             | *)
 (* |-----------------------------:|---|:------------------------------------  *)
 (* |                         set0 |==| $\emptyset$                            *)
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index 78fbbf38d5..430576e6b1 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -16,41 +16,69 @@ From mathcomp Require Import mathcomp_extra signed.
 (**md**************************************************************************)
 (* # Extended real numbers $\overline{R}$                                     *)
 (*                                                                            *)
-(* Given a type R for numbers, \bar R is the type R extended with symbols     *)
-(* -oo and +oo (notation scope: %E), suitable to represent extended real      *)
-(* numbers. When R is a numDomainType, \bar R is equipped with a canonical    *)
-(* porderType and operations for addition/opposite. When R is a               *)
-(* realDomainType, \bar R is equipped with a Canonical orderType.             *)
+(* Given a type R for numbers, `\bar R` is the type `R` extended with symbols *)
+(* `-oo` and `+oo` (notation scope: `%E`), suitable to represent extended     *)
+(* real numbers. When `R` is a `numDomainType`, `\bar R` is equipped with a   *)
+(* canonical `porderType` and operations for addition/opposite. When `R` is a *)
+(* `realDomainType`, `\bar R` is equipped with a canonical `orderType`.       *)
 (*                                                                            *)
 (* Naming convention: in definition/lemma identifiers, "e" stands for an      *)
-(* extended number and "y" and "Ny" for +oo ad -oo respectively.              *)
+(* extended number and "y" and "Ny" for `+oo` and `-oo` respectively.         *)
 (*                                                                            *)
-(* | Coq definitions        |  |                                            | *)
+(* Examples of notations:                                                     *)
+(* | Coq definitions        |  | Meaning                                    | *)
 (* |-----------------------:|--|--------------------------------------------| *)
-(* |               `\bar R` |==| coproduct of `R` and $\{+\infty, -\infty\}$;|*)
-(* |                        |  | notation for extended `(R:Type)`           | *)
+(* |               `\bar R` |==| coproduct of `R` and $\{+\infty, -\infty\}$| *)
+(* |                        |  | notation for `extended (R:Type)`           | *)
 (* |                 `r%:E` |==| injects real numbers into `\bar R`         | *)
-(* |        `+%E, -%E, *%E` |==| addition/opposite/multiplication for extended|*)
-(* |                        |  | reals                                      | *)
+(* |        `+%E, -%E, *%E` |==| addition/opposite/multiplication for       | *)
+(* |                        |  | extended reals                             | *)
 (* | `er_map (f : T -> T')` |==| the `\bar T -> \bar T'` lifting of `f`     | *)
 (* |                `sqrte` |==| square root for extended reals             | *)
-(* |       `` `\| x \|%E `` |==| the absolute value of `x`               | *)
+(* |       `` `\| x \|%E `` |==| the absolute value of `x`                  | *)
 (* |               `x ^+ n` |==| iterated multiplication                    | *)
 (* |               `x *+ n` |==| iterated addition                          | *)
-(* |    `+%dE, (x *+ n)%dE` |==| dual addition/dual iterated addition for   | *)
-(* |                        |  | extended reals ($-\infty + +\infty = +\infty$ instead of $-\infty$)|*)
+(* |    `+%dE, (x *+ n)%dE` |==| dual addition/dual iterated addition       | *)
+(* |                        |  | ($-\infty + +\infty = +\infty$)            | *)
 (* |                        |  | Import DualAddTheory for related lemmas    | *)
-(* |               `x +? y` |==| the addition of the extended real numbers `x` and|*)
-(* |                        |  | and `y` is defined, i.e., it is neither $+\infty - \infty$|*)
+(* |               `x +? y` |==| the addition of `x` and `y` is defined     | *)
+(* |                        |  | it is neither $+\infty - \infty$           | *)
 (* |                        |  | nor $-\infty + \infty$                     | *)
-(* |               `x *? y` |==| the multiplication of the extended real numbers|*)
-(* |                        |  | `x` and `y` is not of the form $0 * +\infty$ or $0 * -\infty$|*)
+(* |               `x *? y` |==| the multiplication of `x` and `y` is not   | *)
+(* |                        |  | of the form $0 * +\infty$ or $0 * -\infty$ | *)
 (* | `(_ <= _)%E`, `(_ < _)%E`,|==| comparison relations for extended reals | *)
 (* | `(_ >= _)%E`, `(_ > _)%E` |  |                                         | *)
 (* | `(\sum_(i in A) f i)%E`|==| bigop-like notation in scope `%E`          | *)
 (* |`(\prod_(i in A) f i)%E`|==| bigop-like notation in scope `%E`          | *)
-(* |   `maxe x y, mine x y` |==| notation for the maximum/minimum of two    | *)
-(* |                        |  | extended real numbers                      | *)
+(* |   `maxe x y, mine x y` |==| notation for the maximum/minimum           | *)
+(*                                                                            *)
+(* Detailed documentation:                                                    *)
+(* ```                                                                        *)
+(*                  \bar R == coproduct of R and {+oo, -oo};                  *)
+(*                            notation for extended (R:Type)                  *)
+(*                    r%:E == injects real numbers into \bar R                *)
+(*           +%E, -%E, *%E == addition/opposite/multiplication for extended   *)
+(*                            reals                                           *)
+(*    er_map (f : T -> T') == the \bar T -> \bar T' lifting of f              *)
+(*                   sqrte == square root for extended reals                  *)
+(*                `| x |%E == the absolute value of x                         *)
+(*                  x ^+ n == iterated multiplication                         *)
+(*                  x *+ n == iterated addition                               *)
+(*       +%dE, (x *+ n)%dE == dual addition/dual iterated addition for        *)
+(*                            extended reals (-oo + +oo = +oo instead of -oo) *)
+(*                            Import DualAddTheory for related lemmas         *)
+(*                  x +? y == the addition of the extended real numbers x and *)
+(*                            and y is defined, i.e., it is neither +oo - oo  *)
+(*                            nor -oo + oo                                    *)
+(*                  x *? y == the multiplication of the extended real numbers *)
+(*                            x and y is not of the form 0 * +oo or 0 * -oo   *)
+(*  (_ <= _)%E, (_ < _)%E, == comparison relations for extended reals         *)
+(*  (_ >= _)%E, (_ > _)%E                                                     *)
+(*   (\sum_(i in A) f i)%E == bigop-like notation in scope %E                 *)
+(*  (\prod_(i in A) f i)%E == bigop-like notation in scope %E                 *)
+(*      maxe x y, mine x y == notation for the maximum/minimum of two         *)
+(*                            extended real numbers                           *)
+(* ```                                                                        *)
 (*                                                                            *)
 (* ## Signed extended real numbers                                            *)
 (* ```                                                                        *)