Split ssralg.v

[pi8027]

Motivation for this change

Following the discussion during a MathComp meeting, I propose splitting ssralg.v into the following files:

• alg_theory/algebra.v contains the (semi)ring, (semi)module, and (semi)algebra structures below unitRingType.
• alg_theory/divalg.v contains the structures with division (unitRingType and above, but below decFieldType).
• alg_theory/decfield.v contains the reflection of the first-order theory of unitRingType, decFieldType, and closedFieldType.
• alg_theory/ssralg.v re-exports the contents of the above files, and contains most of the deprecation abbreviations from old ssralg.v. This file should act as the compatibility layer.

I'm still looking for a better name for alg_theory/algebra.v, but ring.v is currently taken by Algebra Tactics. I think it makes sense to rename ring.v of Algebra Tactics to, say, ring_tactics.v. However, it's going to take a while because we need to go through the following steps:

1. renaming ring.v to ring_tactics.v and deprecating the former in Algebra Tactics,
2. removing the deprecated ring.v in Algebra Tactics (after waiting for at least a few months), and
3. renaming alg_theory/algebra.v to alg_theory/ring.v in MathComp.

I think we should eventually move ring_quotient.v, countalg.v, and finalg.v to alg_theory too. The contents of alg_theory/*.v should eventually be re-exported from alg_theory/all.v (cf. #1505), and then, alg_theory/ssralg.v should probably be deprecated and removed.

This change will probably enable us to:

• add more structures with division: unitSemiRingType, Euclidean domains, etc., and
• reorder the declarations in the same way as order.v: all the structures first, theory, factories, then instances.

Closes #1275.

Dependency

• #1506

Minimal TODO list

• [x] added changelog entries with doc/changelog/make-entry.sh

• [x] added corresponding documentation in the headers
• [x] tried to abide by the contribution guide
• [ ] this PR contains an optimum number of meaningful commits

See this Checklist for details.

Automatic note to reviewers

Read this Checklist.

[pi8027]

Nix CI looks a bit unstable right now, but real-closed is an actual breakage:

File "./theories/ordered_qelim.v", line 443, characters 13-18:
Error: The variable add0r was not found in the current environment.

[pi8027]

Apparently, ordered_qelim.v depends on the reflection stuff defined in ssralg.v and thus imports GRing. So I probably need to reexport the GRing modules for the time being.

[pi8027]

I'm taking advantage of this PR to isolate the deprecation stuff in ssralg.v. Since the largest file (algebra.v) is 4.5k lines long, I'm already quite happy with the result.

[pi8027]

I introduced a new file alg_theory/decfield.v for decFieldType and closedFieldType, and updated the description of the PR.

[pi8027]

This PR is ready. I will add changelog entries.

[pi8027]

I renamed alg_theory to alg.

[CohenCyril]

@proux01 if you also agree, let us merge.