adapt to change in coq2html

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      *)

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. *)

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        *)

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                                         *)
 (*                                                                            *)
 (* ```                                                                        *)

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                                      *)
 (******************************************************************************)
 

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.          *)

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.                       *)

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                               *)
 (******************************************************************************)
 

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.

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.   *)

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     *)

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 *)

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   *)

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  *)

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       *)

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   *)

theories/forms.v

@@ -6,7 +6,7 @@ From mathcomp
 Require Import fieldext.
 From mathcomp Require Import vector.
 
-(***md*************************************************************************)
+(**md**************************************************************************)
 (* # Bilinear forms                                                           *)
 (* (undocumented)                                                             *)
 (******************************************************************************)

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.                                   *)

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        *)

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        *)

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:                     *)

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     *)

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       *)

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 *)

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.   *)