coq-library-undecidability
coq-library-undecidability copied to clipboard
uds-psl
coqdoc / website
Currently, our coqdoc is a complete mess.
I don't know how to fix this in a good way, and it's well possible that we want to ignore the issue for now.
Alternatively, we can in a first step remove all coqdoc headings generation by replacing (** with (* everywhere in the code. In a second step, we can then add coqdoc headings in the Problem.v and Problem_undec.v files only. That way, the coqdoc toc.html file gives a good overview over the library.
Downside: For this to work well, we would have to move the Problem.v and Problem_undec.v lines in _CoqProject to be in the right order.
the order of files in _CoqProject has no influence on anything I know except on the coqdoc (I thought it does someting with compilation order, but that is not the case appearently). So reordering everything would be possible.
@mrhaandi @DmxLarchey would you be fine with such a change?
Lots of files would have to be touched, so I'm not I can finish it today, but if it's possible it would be neat to ship the library with clean coqdoc.
would you be fine with such a change?
I support it. Useful documentation is worth the effort.
Well of course I do support the effort as well but I do not think there is a need to rush to ship it with the release.
