Split Gallina, Gallina ext and most of CIC chapters into multiple pages.

[Zimmi48]

This PR is a very rough splitting of the Gallina, Gallina extensions and CIC chapters into multiple pages. This is virtually only cut and paste with no adaptation to the context (just the minimum required to make it compile).

The main point of the PR is to gather feedback on the general structure ASAP and to identify the parts that will need the more effort to make acceptable in a released version.

This is a change of strategy compared to #12172, which took one week to prepare and one more week to review and merge. Given that we are just one month away from releasing 8.12+beta1 (by which time, it would be preferable to have conducted all significant changes to the refman) and two months away from releasing 8.12.0, it would not be realistic to continue at the same pace.

cc @jfehrle @mattam82 @herbelin @JasonGross and anyone else who is interested.

Core language index: https://coq.gitlab.io/-/coq/-/jobs/554084025/artifacts/_install_ci/share/doc/coq/sphinx/html/language/core/index.html
Language extensions index: https://coq.gitlab.io/-/coq/-/jobs/554084025/artifacts/_install_ci/share/doc/coq/sphinx/html/language/extensions/index.html

[jfehrle]

AFAICT nothing was lost. Let's go with this for now--thought there may be further refinements later.

[Zimmi48]

I've updated the PR to preserve the history of the sections that were moved.

Compared to the previous version, the changes are as follows:

• less about universes in the sorts section (more in the universe polymorphism section instead: we should likely rename it into just "universes");
• the section on impredicative set was left in CIC for now (now a section titled "Typing rules");
• in sections on Assumptions and on Definitions, the term constructs are moved before the top-level commands;
• type casts moved from Assumptions to Definitions (I'm unsure this will be its definite location, maybe it would be more appropriate in "Typing rules" but for now this section is very theoretical).
• slightly different order of sections in the Core language chapter.

Note that given the size of the changes, conflicts are bound to appear very quickly, so it would be good to merge ASAP (cc @cpitclaudel). And given the number of merge commits, this is impossible to backport, so should definitely go in before the branching.

[Zimmi48]

Note that this PR doesn't contain any new content, just minimal fixes to make things hold together. Some new files will need a bit of rewording but this will be done as a later step, before the 8.12.0 release.

[Zimmi48]

ping @cpitclaudel