diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index a16b493e5..3bf3f9df8 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -55,6 +55,7 @@ From mathcomp Require Import mathcomp_extra boolp.
 (* |                 trivIset D F |==| F is a sequence of pairwise disjoint | *)
 (* |                              |  | sets indexed over the domain D       | *)
 (*                                                                            *)
+(* Details:                                                                   *)
 (* ## Sets                                                                    *)
 (* ```                                                                        *)
 (*                       set T == type of sets on T                           *)