Add "coqdoc_header" and "coqdoc_footer" fields.

[rlepigre]

This is an attempt at fixing #11017.

Although I have a working test-case, I have not done much testing so far. I'd appreciate early feedback anyway, if you can find the time to have a quick look @Alizter, @ejgallego.

What remains to be done:

• Check for language version in the new fields.
• Update the documentation.
• Add change log entry.

[Alizter]

While we are here, shall we add a field_b_o for toc. It should default to enabled, but we can allow it to be set like header and footer.

[Alizter]

We should add a test where the header file comes as the target of another rule. We need to check that the dependencies are being correctly handled.

Variable expansion is also another one that should be checked, but I'm not certain what the best way to do that is yet.

[rlepigre]

We should add a test where the header file comes as the target of another rule. We need to check that the dependencies are being correctly handled.

Variable expansion is also another one that should be checked, but I'm not certain what the best way to do that is yet.

@Alizter I added a test that should exercise both at once.

While we are here, shall we add a field_b_o for toc. It should default to enabled, but we can allow it to be set like header and footer.

I'm not sure what you have in mind here, actually. Can't we just use the (coqdoc_flags ...) field for that?

[Alizter]

While we are here, shall we add a field_b_o for toc. It should default to enabled, but we can allow it to be set like header and footer.

I'm not sure what you have in mind here, actually. Can't we just use the (coqdoc_flags ...) field for that?

we already set --toc by default. I thought it might be a good idea to introduce a field for that as well. It's not a priority however, so you can disregard that comment.

[Alizter]

I played around a bit with dropping the directory here, and I couldn't find a good way to do it. I'm not too worried about this.

[rlepigre]

Yeah, I wasn't sure what to do there.

[Alizter]

Does it make sense to pass these flags when in latex mode? I think this might error out coqdoc. Should be simple to add a test for that.

[rlepigre]

Does it make sense to pass these flags when in latex mode? I think this might error out coqdoc. Should be simple to add a test for that.

The option is actually ignored (I had tested this), but I guess there is no point in introducing potential dependencies for the latex documentation. I pushed a fix.