From 8ac72cc8f52732082cb7d9941b641407fe72618a 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 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 *)