Closed thomas-lamiaux closed 5 months ago
The coqdoc
output of (** * A single star title *)
is really big.
As far as I know, it's only used for the title of the document.
@Villetaneuse does it look big too with JsCoq ?
It really depends on your css
, but I'm quite sure it really semantically means "title of the document", a bit like one #
header in md
is for the title.
Ok, I'll add it in the guidelines
In the tutorial for Equations, I have used the following coqdoc syntax :
I have noticed #11 uses
should we fix a convention so that all files look the same once they'll be a web interface ?