coqdoc / website

[yforster]

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.

[fakusb]

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.

[yforster]

@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.

[mrhaandi]

would you be fine with such a change?

I support it. Useful documentation is worth the effort.

[DmxLarchey]

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.