xavierleroy / coq2html

An HTML documentation generator for Coq source files
GNU General Public License v2.0
30 stars 11 forks source link

Missing indent before Proof #7

Closed Vertmo closed 3 years ago

Vertmo commented 3 years ago

This is a detail, but with the current HTML generation, the first line of Proof located under Module or Section are not properly indented. For instance:

Module MyMod.
  Lemma taut: forall A : Prop, A -> A.
  Proof.
    auto.
  Qed.
End MyMod.

Is exported as: 2021-04-07-121042_304x95_scrot

Here is the result after my modifications: 2021-04-07-124959_281x94_scrot

The Qed line is still a bit skewed to the left (due to the proof script being in a smaller font), which is bothering me, but I'm not sure how to fix it...