adapt to change in coq2html

math-comp · Jan 14, 2024 · 728a9df · 728a9df
1 parent bf9651f
commit 728a9df
Show file tree

Hide file tree

Showing 38 changed files with 52 additions and 52 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.   *)