minimal changes to documentation to test coq2html

[affeldt-aist]

Motivation for this change

The goal of this PR is to test a fork of coq2html to document MathComp-Analysis
using mardown.

fixes #1114

fixes #1071

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[proux01]

@affeldt-aist @yoshihiro503 The doc generated at https://yoshihiro503.github.io/coq2html/ looks really great and this seems a worthwile replacement of coqdoc, here are just a few minor comments by looking at it:

• very minor: HTML title of that page: "Module $NAME"
• minor but probably easy to fix: missing purple keywords
  • Set Implicit Arguments.
  • Unset Strict Implicit
  • Unset Printing Implicit Defensive
  • Number Notation
  • Declare Scope
  • Delimit Scope
  • Bind Scope
  • Local
• very minor: some links to stdlib notations are partly broken (for instance https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Init.Specif.html#::type_scope:'{'_x_':'_x_'|'_x_'&'_x_'}' or https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.ssr.ssrfun.html#::fun_scope:x_'=1'_x )
• very minor: some links to mathcomp seem broken: https://math-comp.github.io/htmldoc/mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.zmodType
  (looks like it's not a coq2html bug but the fact that doc of Analysis master (still on MC1) should link to the doc of MC1 not MC master (MC2))
• minor: some internal links seem broken: https://yoshihiro503.github.io/coq2html/mathcomp.classical.mathcomp_extra.html#P:4 works great but https://yoshihiro503.github.io/coq2html/mathcomp.classical.mathcomp_extra.html#T:2 doesn't
• serious: links to section variables can be broken, for instance https://yoshihiro503.github.io/coq2html/mathcomp.analysis.measure.html#classes.G
• serious: some links to HB defined types are broken, for instance https://yoshihiro503.github.io/coq2html/mathcomp.analysis.measure.html#ringOfSetsType
• not sure why HB.mixin and some HB.instance get displayed in red but not all HB.structure (I would either display nothing in red or all of the commands in https://github.com/math-comp/hierarchy-builder/blob/master/structures.v with some link to that file in addition to the color
• very minor: in #[short(type=semiRingOfSetsType)], an extra spurious space is introduced after short

Overall, the only features I can see missing from coqdoc (but we don't use them in mathcomp) are:

• the table of content generated from the first title of each file, following the order of the _CoqProject
• the ability to easily link to constants in the comments (by just surrounding them with [ and ]

[affeldt-aist]

Here is the result of the rebase:

• https://math-comp.github.io/analysis/htmldoc_0_6_7/index.html
  (this is a temporary placeholder, I will override it with the release)
• I have recorded the issues you have reported here:
  https://github.com/affeldt-aist/coq2html/issues

[proux01]

BTW, are th three stars before md mandatory? why not just two? (coqdoc syntax is (** IIRC so not sure a third star is needed)

[affeldt-aist]

That's arbitrary. No strong reason I think.

[proux01]

Here we don't really care because there are stars all along the line. But in case we wouldn't use block comments, with stars all around, but just start (* and closing *) syntax, the less stars the better I'd say.

[affeldt-aist]

We'll clarify this on Friday.