...and "Defined" can end one.

This can be useful for learning / teaching.

Marco Perronet authored 5 years ago and Björn Brandenburg committed 5 years ago

... to get support for proofs started by `Next Obligation`.

1) rely on patch to actually patch the Makefile
2) move ineffective 'sed' hackery related to 'make validate'

Re 2), the sed script didn't actually modify the Makefile anyway
(unlear how long it has been ineffective), so let's just remove it.

The mathcomp coqdoc documentation is now at:

   https://math-comp.github.io/htmldoc/

Tweak our Makefile accordingly.

Also switch how this is patched into the Makefile while we're at it.

...while at it, remove some old cruft in there.

Marco Perronet authored 5 years ago and Björn Brandenburg committed 5 years ago

Add the `htmlpretty` target to the Makefile to generate prettier documentation,
based on the CoqdocJS project.

     https://www.ps.uni-saarland.de/~ttebbi/coqdocjs/

     https://github.com/tebbi/coqdocjs

Many thanks to Tobias Tebbi for creating CoqdocJS.