diff --git a/classical/boolp.v b/classical/boolp.v
index eab865657..7acb9098c 100644
--- a/classical/boolp.v
+++ b/classical/boolp.v
@@ -7,7 +7,7 @@
 
 From mathcomp Require Import all_ssreflect.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Classical Logic                                                          *)
 (*                                                                            *)
 (* This file provides the axioms of classical logic and tools to perform      *)
diff --git a/classical/cardinality.v b/classical/cardinality.v
index 536a5b4fa..d9ce6b8db 100644
--- a/classical/cardinality.v
+++ b/classical/cardinality.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Cardinality                                                              *)
 (*                                                                            *)
 (* This file provides an account of cardinality properties of classical sets. *)
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index ad60a6eaf..ddebf5da0 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
 From mathcomp Require Import ssrint interval.
 From mathcomp Require Import mathcomp_extra boolp.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Set Theory                                                               *)
 (*                                                                            *)
 (* This file develops a basic theory of sets and types equipped with a        *)
diff --git a/classical/fsbigop.v b/classical/fsbigop.v
index 2b68d7286..23086e007 100644
--- a/classical/fsbigop.v
+++ b/classical/fsbigop.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Finitely-supported big operators                                         *)
 (*                                                                            *)
 (* ```                                                                        *)
diff --git a/classical/functions.v b/classical/functions.v
index db857e22e..491b639d4 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -7,7 +7,7 @@ Add Search Blacklist "__functions_".
 Add Search Blacklist "_factory_".
 Add Search Blacklist "_mixin_".
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Theory of functions                                                      *)
 (*                                                                            *)
 (* This file provides a theory of functions $f : A\to B$ whose domain $A$     *)
@@ -377,7 +377,7 @@ Notation "A <~> B" := {bij A >-> B} (at level 70) : type_scope.
 Notation "A <<~> B" := {splitbij A >-> B} (at level 70) : type_scope.
 End ShortFunSyntax.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Theory                                                                  *)
 (******************************************************************************)
 
@@ -1006,7 +1006,7 @@ HB.instance Definition _ (f : {inj A >-> rT}) :=
   SurjFun_Inj.Build _ _ _ _ [fun f in A] 'inj_f.
 End Inverses.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Simple Factories                                                        *)
 (******************************************************************************)
 
@@ -1101,7 +1101,7 @@ Proof.
 by move/in1W/(@funPsplitsurj _ _ _ _ [fun of totalfun f] [fun of totalfun g]).
 Qed.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Instances                                                               *)
 (******************************************************************************)
 
@@ -1461,7 +1461,7 @@ HB.instance Definition _ n := Can2.Build _ _ setT setT (@ordII n)
    (fun _ _ => I) (fun _ _ => I) (in1W ordIIK) (in1W IIordK).
 HB.instance Definition _ n := SplitBij.copy (@IIord n) (ordII^-1).
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Glueing                                                                 *)
 (******************************************************************************)
 
@@ -1609,7 +1609,7 @@ HB.instance Definition _ := empty_canv_subproof.
 
 End empty.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Theory of surjection                                                    *)
 (******************************************************************************)
 
@@ -1822,7 +1822,7 @@ Definition phant_bijTT aT rT (f : {bij [set: aT] >-> [set: rT]})
 Notation "''bijTT_'  f" := (phant_bijTT (Phantom (_ -> _) f)) : form_scope.
 #[global] Hint Extern 0 (bijective _) => solve [apply: bijTT] : core.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Patching and restrictions                                               *)
 (******************************************************************************)
 
@@ -1906,7 +1906,7 @@ do 2![case: ifPn => //]; rewrite !in_setE => Di Dj Fix Fjx.
 by apply: FDtriv => //; exists x.
 Qed.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Restriction of domain and codomain                                      *)
 (******************************************************************************)
 
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index ea0f127ee..3b1a5a188 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -9,7 +9,7 @@ Coercion choice.Choice.mixin : choice.Choice.class_of >-> choice.Choice.mixin_of
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import finset interval.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # MathComp extra                                                           *)
 (*                                                                            *)
 (* This files contains lemmas and definitions missing from MathComp.          *)
diff --git a/classical/set_interval.v b/classical/set_interval.v
index 5b290fc5f..7d716fa91 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -4,7 +4,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From HB Require Import structures.
 From mathcomp Require Import functions.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Sets and Intervals                                                       *)
 (*                                                                            *)
 (* This files contains lemmas about sets and intervals.                       *)
diff --git a/theories/Rstruct.v b/theories/Rstruct.v
index de38616b3..90945aa50 100644
--- a/theories/Rstruct.v
+++ b/theories/Rstruct.v
@@ -21,7 +21,7 @@ the economic rights, and the successive licensors have only limited
 liability. See the COPYING file for more details.
 *)
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Compatibility with the real numbers of Coq                               *)
 (******************************************************************************)
 
diff --git a/theories/cantor.v b/theories/cantor.v
index 9a92dd486..439c41e34 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -6,7 +6,7 @@ From mathcomp Require Import cardinality.
 Require Import reals signed topology.
 From HB Require Import structures.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # The Cantor Space and Applications                                        *)
 (*                                                                            *)
 (* This file develops the theory of the Cantor space, that is bool^nat with   *)
@@ -77,7 +77,7 @@ split.
 - exact: cantor_zero_dimensional.
 Qed.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Part 1                                                                  *)
 (*                                                                            *)
 (* A tree here has countable levels, and nodes of type `K n` on the nth       *)
@@ -241,7 +241,7 @@ Qed.
 
 End topological_trees.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Part 2                                                                  *)
 (* We can use `tree_map_props` to build a homeomorphism from the              *)
 (* cantor_space to a Cantor-like space T.                                     *)
@@ -339,7 +339,7 @@ Qed.
 
 End TreeStructure.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Part 3: Finitely branching trees are Cantor-like                        *)
 (******************************************************************************)
 Section FinitelyBranchingTrees.
@@ -375,7 +375,7 @@ End FinitelyBranchingTrees.
 
 Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* ## Part 4: Building a finitely branching tree to cover `T`                 *)
 (******************************************************************************)
 Section alexandroff_hausdorff.
diff --git a/theories/charge.v b/theories/charge.v
index fe47963c1..f2fb02d85 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -7,7 +7,7 @@ From HB Require Import structures.
 Require Import reals ereal signed topology numfun normedtype sequences.
 Require Import esum measure realfun lebesgue_measure lebesgue_integral.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Charges                                                                  *)
 (*                                                                            *)
 (* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.   *)
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index aeb789bb1..6b6d0e1e7 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -13,7 +13,7 @@ From mathcomp Require Import all_ssreflect all_algebra finmap.
 From mathcomp Require Import mathcomp_extra.
 Require Import signed.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Extended real numbers $\overline{R}$                                     *)
 (*                                                                            *)
 (* Given a type R for numbers, \bar R is the type R extended with symbols     *)
diff --git a/theories/convex.v b/theories/convex.v
index 0ae78af0e..dea32cb4f 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -7,7 +7,7 @@ Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
 Require Import realfun itv.
 From HB Require Import structures.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Convexity                                                                *)
 (*                                                                            *)
 (* This file provides a small account of convexity using convex spaces, to be *)
diff --git a/theories/derive.v b/theories/derive.v
index fd3d2fa0b..ccce3ec2d 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals signed topology prodnormedzmodule normedtype landau forms.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Differentiation                                                          *)
 (*                                                                            *)
 (* This file provides a theory of differentiation. It includes the standard   *)
diff --git a/theories/ereal.v b/theories/ereal.v
index 0ba971322..9a0bcd033 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -11,7 +11,7 @@ From mathcomp Require Import fsbigop cardinality set_interval.
 Require Import reals signed topology.
 Require Export constructive_ereal.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Extended real numbers, classical part ($\overline{\mathbb{R}}$)          *)
 (*                                                                            *)
 (* This is an addition to the file constructive_ereal.v with classical logic  *)
diff --git a/theories/esum.v b/theories/esum.v
index e0c552a39..69869857b 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -4,7 +4,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology sequences normedtype numfun.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Summation over classical sets                                            *)
 (*                                                                            *)
 (* This file provides a definition of sum over classical sets and a few       *)
diff --git a/theories/exp.v b/theories/exp.v
index 75bb53849..08e524ff4 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -7,7 +7,7 @@ Require Import reals ereal.
 Require Import signed topology normedtype landau sequences derive realfun.
 Require Import itv convex.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Theory of exponential/logarithm functions                                *)
 (*                                                                            *)
 (* This file defines exponential and logarithm functions and develops their   *)
diff --git a/theories/forms.v b/theories/forms.v
index ce60998bb..da347889f 100644
--- a/theories/forms.v
+++ b/theories/forms.v
@@ -6,7 +6,7 @@ From mathcomp
 Require Import fieldext.
 From mathcomp Require Import vector.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Bilinear forms                                                           *)
 (* (undocumented)                                                             *)
 (******************************************************************************)
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 7d138d9d9..86308c02e 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -7,7 +7,7 @@ Require Import signed reals ereal topology normedtype sequences real_interval.
 Require Import esum measure lebesgue_measure lebesgue_integral numfun exp.
 Require Import convex itv.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Hoelder's Inequality                                                     *)
 (*                                                                            *)
 (* This file provides Hoelder's inequality.                                   *)
diff --git a/theories/itv.v b/theories/itv.v
index bc46e7ac3..49b9e852a 100644
--- a/theories/itv.v
+++ b/theories/itv.v
@@ -5,7 +5,7 @@ From mathcomp Require Import interval.
 From mathcomp Require Import mathcomp_extra boolp.
 Require Import signed.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Numbers within an intervel                                               *)
 (*                                                                            *)
 (* This file develops tools to make the manipulation of numbers within        *)
diff --git a/theories/kernel.v b/theories/kernel.v
index 29138aad4..1d4fefa3e 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -6,7 +6,7 @@ From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology normedtype sequences esum measure.
 Require Import numfun lebesgue_measure lebesgue_integral.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Kernels                                                                  *)
 (*                                                                            *)
 (* This file provides a formation of kernels, s-finite kernels, finite        *)
diff --git a/theories/landau.v b/theories/landau.v
index cacb7834d..1b19ad84d 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import ereal reals signed topology normedtype prodnormedzmodule.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Bachmann-Landau notations: $f=o(e)$, $f=O(e)$                            *)
 (*                                                                            *)
 (* This library is very asymmetric, in multiple respects:                     *)
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 720ee910e..362f7dc41 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -6,7 +6,7 @@ From mathcomp Require Import cardinality fsbigop .
 Require Import signed reals ereal topology normedtype sequences real_interval.
 Require Import esum measure lebesgue_measure numfun.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Lebesgue Integral                                                        *)
 (*                                                                            *)
 (* This file contains a formalization of the Lebesgue integral. It starts     *)
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 1893f1bab..b298482b3 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -8,7 +8,7 @@ From HB Require Import structures.
 Require Import sequences esum measure real_interval realfun exp.
 Require Export lebesgue_stieltjes_measure.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Lebesgue Measure                                                         *)
 (*                                                                            *)
 (* This file contains a formalization of the Lebesgue measure using the       *)
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index 19687c9e4..d8c9a0445 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -7,7 +7,7 @@ From mathcomp.classical Require Import functions fsbigop cardinality.
 Require Import reals ereal signed topology numfun normedtype sequences esum.
 Require Import real_interval measure realfun.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Lebesgue Stieltjes Measure                                               *)
 (*                                                                            *)
 (* This file contains a formalization of the Lebesgue-Stieltjes measure using *)
diff --git a/theories/measure.v b/theories/measure.v
index 300d4f0f7..ca1a15e64 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -5,7 +5,7 @@ From mathcomp Require Import cardinality fsbigop .
 Require Import reals ereal signed topology normedtype sequences esum numfun.
 From HB Require Import structures.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Measure Theory                                                           *)
 (*                                                                            *)
 (* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.   *)
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 303bd1b83..75a71e00d 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality set_interval Rstruct.
 Require Import ereal reals signed topology prodnormedzmodule.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Norm-related Notions                                                     *)
 (*                                                                            *)
 (* This file extends the topological hierarchy with norm-related notions.     *)
@@ -20,7 +20,7 @@ Require Import ereal reals signed topology prodnormedzmodule.
 (*                                   f has type X -> \bar R.                  *)
 (*                                   F has type set (set X).                  *)
 (*                                                                            *)
-(* ## Normed Topological Abelian groups:                                      *)
+(* ## Normed topological abelian groups                                       *)
 (* ```                                                                        *)
 (*  pseudoMetricNormedZmodType R  == interface type for a normed topological  *)
 (*                                   Abelian group equipped with a norm       *)
diff --git a/theories/nsatz_realtype.v b/theories/nsatz_realtype.v
index 5533db617..218346e2b 100644
--- a/theories/nsatz_realtype.v
+++ b/theories/nsatz_realtype.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum.
 From mathcomp Require Import boolp.
 Require Import reals ereal.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # nsatz for realType                                                       *)
 (*                                                                            *)
 (* This file registers the ring corresponding to the MathComp-Analysis type   *)
diff --git a/theories/numfun.v b/theories/numfun.v
index 0ff8585b7..03e423e5e 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop.
 From mathcomp Require Import functions cardinality set_interval.
 Require Import signed reals ereal topology normedtype sequences.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Numerical functions                                                      *)
 (*                                                                            *)
 (* This file provides definitions and lemmas about numerical functions.       *)
diff --git a/theories/probability.v b/theories/probability.v
index f809177b9..6b332baca 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -8,7 +8,7 @@ Require Import exp numfun lebesgue_measure lebesgue_integral.
 Require Import reals ereal signed topology normedtype sequences esum measure.
 Require Import exp numfun lebesgue_measure lebesgue_integral.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Probability                                                              *)
 (*                                                                            *)
 (* This file provides basic notions of probability theory. See measure.v for  *)
diff --git a/theories/prodnormedzmodule.v b/theories/prodnormedzmodule.v
index 84f78f603..6022f6a33 100644
--- a/theories/prodnormedzmodule.v
+++ b/theories/prodnormedzmodule.v
@@ -1,7 +1,7 @@
 From mathcomp Require Import all_ssreflect fingroup ssralg poly ssrnum.
 Require Import signed.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* This file equips the product of two normedZmodTypes with a canonical       *)
 (* normedZmodType structure. It is a short file that has been added here for  *)
 (* convenience during the rebase of MathComp-Analysis on top of MathComp 1.1. *)
diff --git a/theories/real_interval.v b/theories/real_interval.v
index abde9b5ff..fcd074f8a 100644
--- a/theories/real_interval.v
+++ b/theories/real_interval.v
@@ -6,7 +6,7 @@ From mathcomp Require Export set_interval.
 From HB Require Import structures.
 Require Import reals ereal signed topology normedtype sequences.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Sets and intervals on $\overline{\mathbb{R}}$                            *)
 (******************************************************************************)
 
diff --git a/theories/realfun.v b/theories/realfun.v
index c2101f7c0..a07a22ee2 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -7,7 +7,7 @@ Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
 Require Import sequences real_interval.
 From HB Require Import structures.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Real-valued functions over reals                                         *)
 (*                                                                            *)
 (* This file provides properties of standard real-valued functions over real  *)
diff --git a/theories/reals.v b/theories/reals.v
index 02c83c159..a7fb89377 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -5,7 +5,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # An axiomatization of real numbers $\mathbb{R}$                           *)
 (*                                                                            *)
 (* This file provides a classical axiomatization of real numbers as a         *)
diff --git a/theories/sequences.v b/theories/sequences.v
index ab428f080..c200d896b 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import set_interval.
 Require Import reals ereal signed topology normedtype landau.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Definitions and lemmas about sequences                                   *)
 (*                                                                            *)
 (* The purpose of this file is to gather generic definitions and lemmas about *)
diff --git a/theories/signed.v b/theories/signed.v
index 9f611a3e7..29a2faa55 100644
--- a/theories/signed.v
+++ b/theories/signed.v
@@ -3,7 +3,7 @@ From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
 From mathcomp Require Import mathcomp_extra.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Positive, non-negative numbers, etc.                                     *)
 (*                                                                            *)
 (* This file develops tools to make the manipulation of numbers with a known  *)
diff --git a/theories/summability.v b/theories/summability.v
index 08f0b4138..d86502b9e 100644
--- a/theories/summability.v
+++ b/theories/summability.v
@@ -5,7 +5,7 @@ From mathcomp Require Import interval zmodp.
 From mathcomp Require Import boolp classical_sets.
 Require Import ereal reals Rstruct signed topology normedtype.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* (undocumented experiment)                                                  *)
 (******************************************************************************)
 
diff --git a/theories/topology.v b/theories/topology.v
index 1cc626adf..31b5854ff 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -4,7 +4,7 @@ From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
 Require Import reals signed.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Filters and basic topological notions                                    *)
 (*                                                                            *)
 (* This file develops tools for the manipulation of filters and basic         *)
@@ -40,7 +40,7 @@ Require Import reals signed.
 (*                                                                            *)
 (******************************************************************************)
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # 1. Filters                                                               *)
 (*                                                                            *)
 (* ## Structure of filter                                                     *)
@@ -202,7 +202,7 @@ Require Import reals signed.
 (*                                                                            *)
 (******************************************************************************)
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # 2. Basic topological notions                                             *)
 (*                                                                            *)
 (* ## Mathematical structures                                                 *)
diff --git a/theories/trigo.v b/theories/trigo.v
index efc2dfd70..e540c5733 100644
--- a/theories/trigo.v
+++ b/theories/trigo.v
@@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals ereal nsatz_realtype signed topology normedtype landau.
 Require Import sequences derive realfun exp.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Theory of trigonometric functions                                        *)
 (*                                                                            *)
 (* This file provides the definitions of basic trigonometric functions and    *)