The mathcomp coqdoc documentation is now at:

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

Tweak our Makefile accordingly.

Maxime Lesourd authored 5 years ago and Björn Brandenburg committed 5 years ago

- Added unfolding lemmas to basic_facts/ideal
- Fixed proofs depending on the previous definition using unfolding lemmas

The changes follow the discussion in Paris.

As discussed in #57.

As discussed at the RT-PROOFS meeting in Paris, proof terms should not
have a name so that we don't actually directly depend on them in
proofs. This patch removes the explicit name of the proof term in the
readiness type class and introduces an equivalent lemma.

If there are breaking changes coming in ssreflect, it would be nice to
know early.

This avoids the need to use @-notation when establishing platform
properties (e.g., in facts about ideal schedules).

Thanks to Maxime for the suggestion.

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

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

Pierre Roux authored 5 years ago and Björn Brandenburg committed 5 years ago

We no longer support Coq 8.8.

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.

Rationale: reserve the behavior folder for trace-based semantics.

These lemmas really constitute an analysis of the basic consequences
arising from the chosen semantics and hence logically belong to the
"analysis" part of Prosa.

Sergey Bozhko authored 5 years ago and Björn Brandenburg committed 5 years ago

Also removes an unnecessary module in rt.util.epsilon.