search

affeldt-aist / coq2html

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

rendering breaks without `Proof` command #29

Closed affeldt-aist closed 5 months ago

affeldt-aist commented 6 months ago

One could claim that scripts ought to start with Proof but what about when this is a tactic-based definition this?

see https://yoshihiro503.github.io/coq2html/monae/monae.example_typed_store.html for example

@garrigue

affeldt-aist commented 6 months ago

fyi @yoshihiro503

affeldt-aist commented 5 months ago

This has been fixed by commit https://github.com/affeldt-aist/coq2html/commit/ce863714a627bee3d77a2abe511166887b3d5e43