Finishes Poly chapter.
The start of MoreCoq.