From 4e3c4739a09f3b5c5e1f7ce051bdf79dde821ff3 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Sun, 14 Jan 2024 17:40:35 +0900 Subject: [PATCH] adapt to change in coq2html (#1148) --- classical/boolp.v | 2 +- classical/cardinality.v | 2 +- classical/classical_sets.v | 2 +- classical/fsbigop.v | 2 +- classical/functions.v | 16 ++++++++-------- classical/mathcomp_extra.v | 2 +- classical/set_interval.v | 2 +- theories/Rstruct.v | 2 +- theories/cantor.v | 10 +++++----- theories/charge.v | 2 +- theories/constructive_ereal.v | 2 +- theories/convex.v | 2 +- theories/derive.v | 2 +- theories/ereal.v | 2 +- theories/esum.v | 2 +- theories/exp.v | 2 +- theories/forms.v | 2 +- theories/hoelder.v | 2 +- theories/itv.v | 2 +- theories/kernel.v | 2 +- theories/landau.v | 2 +- theories/lebesgue_integral.v | 2 +- theories/lebesgue_measure.v | 2 +- theories/lebesgue_stieltjes_measure.v | 2 +- theories/measure.v | 2 +- theories/normedtype.v | 4 ++-- theories/nsatz_realtype.v | 2 +- theories/numfun.v | 2 +- theories/probability.v | 2 +- theories/prodnormedzmodule.v | 2 +- theories/real_interval.v | 2 +- theories/realfun.v | 2 +- theories/reals.v | 2 +- theories/sequences.v | 2 +- theories/signed.v | 2 +- theories/summability.v | 2 +- theories/topology.v | 6 +++--- theories/trigo.v | 2 +- 38 files changed, 52 insertions(+), 52 deletions(-) diff --git a/classical/boolp.v b/classical/boolp.v index 720114a0e..0f5864740 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -7,7 +7,7 @@ From HB Require Import structures. 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 a9f63f07b..2cce9b33a 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 649259bef..5d586a362 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg matrix finmap 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 b27ae2eda..18b4d06fb 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 fcd3ce38c..ace873725 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$ *) @@ -378,7 +378,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 *) (******************************************************************************) @@ -1007,7 +1007,7 @@ HB.instance Definition _ (f : {inj A >-> rT}) := SurjFun_Inj.Build _ _ _ _ [fun f in A] 'inj_f. End Inverses. -(***md*************************************************************************) +(**md**************************************************************************) (* ## Simple Factories *) (******************************************************************************) @@ -1102,7 +1102,7 @@ Proof. by move/in1W/(@funPsplitsurj _ _ _ _ [fun of totalfun f] [fun of totalfun g]). Qed. -(***md*************************************************************************) +(**md**************************************************************************) (* ## Instances *) (******************************************************************************) @@ -1462,7 +1462,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 *) (******************************************************************************) @@ -1612,7 +1612,7 @@ HB.instance Definition _ := empty_canv_subproof. End empty. -(***md*************************************************************************) +(**md**************************************************************************) (* ## Theory of surjection *) (******************************************************************************) @@ -1825,7 +1825,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 *) (******************************************************************************) @@ -1909,7 +1909,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 e55a0623f..dbf90a224 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -8,7 +8,7 @@ From mathcomp Require choice. 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 046294944..7d13ca4bb 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 c30ee008f..3ce44ea26 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 c206bd441..11e37fecf 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 *) @@ -128,7 +128,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 *) @@ -292,7 +292,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. *) @@ -391,7 +391,7 @@ Qed. End TreeStructure. -(***md*************************************************************************) +(**md**************************************************************************) (* ## Part 3: Finitely branching trees are Cantor-like *) (******************************************************************************) Section FinitelyBranchingTrees. @@ -422,7 +422,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 bd1ed1486..30b2d11b0 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 36ecb9cbe..6c3c0643b 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -14,7 +14,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 126dbf0f7..d9bf76a32 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 7e34a4140..6edda28fa 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -4,7 +4,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 cc80157a4..896c4fc7e 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 22848b4f0..d963a52fd 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 98a395d26..a92627b56 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 4de08aa56..fb8f7956f 100644 --- a/theories/forms.v +++ b/theories/forms.v @@ -7,7 +7,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 4998346bd..2385f9e1f 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 48b27d7d8..2911b9299 100644 --- a/theories/itv.v +++ b/theories/itv.v @@ -6,7 +6,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 c7cade8c2..e4b3e25e3 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 ac6672ad8..c9fb5b13a 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -4,7 +4,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 7a61b8cbb..8b0893855 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 39c7305a3..a29b5398f 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 7894158ea..b25548a94 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 8c7bfd7e0..3aacd9130 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 714078c38..66c9dac3e 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -6,7 +6,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. *) @@ -21,7 +21,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 4b75f6744..7774ff3f0 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 5000c1561..6c4b8e571 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 84d36e863..199cdf769 100644 --- a/theories/prodnormedzmodule.v +++ b/theories/prodnormedzmodule.v @@ -2,7 +2,7 @@ From HB Require Import structures. 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 1da307ace..cc90e5e51 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 8fe14a836..3a1cdfcc3 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 8226761cf..79e403811 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 1611f968e..0d3f80270 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 fd23bb208..a8959485e 100644 --- a/theories/signed.v +++ b/theories/signed.v @@ -4,7 +4,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 0b30f5313..09915bb10 100644 --- a/theories/summability.v +++ b/theories/summability.v @@ -6,7 +6,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 3a5217f9e..df5e6d2a6 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -5,7 +5,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 *) @@ -41,7 +41,7 @@ Require Import reals signed. (* *) (******************************************************************************) -(***md*************************************************************************) +(**md**************************************************************************) (* # 1. Filters *) (* *) (* ## Structure of filter *) @@ -203,7 +203,7 @@ Require Import reals signed. (* *) (******************************************************************************) -(***md*************************************************************************) +(**md**************************************************************************) (* # 2. Basic topological notions *) (* *) (* ## Mathematical structures *) diff --git a/theories/trigo.v b/theories/trigo.v index 2e86366ed..709eabf1f 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 *)