[Corelib] Retrieve ring/field/micromega computational part from Stdlib

[proux01]

This way it can be used by other libraries than just Stdlib.
Maybe more importantly, having the datastructures closer from the OCaml plugin will ease further developments of micromega.
See rocq-prover/stdlib#207 for the adaptation in Stdlib

Scheduled for discussion on rocq call 2025-09-23

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

[proux01]

Cc @fajb

[SkySkimmer]

What prompted this?

[proux01]

For the context: when giving Stdlib it's own repository, we applied a simple rule: keep .ml files in the rocq repository and .v files in the new stdlib repository. We already knew that this was leaving room for improvement, with the micromega plugin referencing constants in another repository. This is such an improvement.
It is not a definitive solution however, the reifier of micromega for Stdlib terms remains implemented in the ocaml plugin whereas it should probably ideally be implemented in some extension language (like Ltac2) in the stdlib repository.

[proux01]

Thinking a bit more about it, maybe a good solution would be to have a dedicated repo for micromega, hosting the plugin and definitions in the current PR, this way:

• each version of micromega could support a few consecutive versions of Rocq
• each user library could peek a single version of micromega they support, and could then adapt to micromega evolutions at its own pace, without needing any conditional compilation

This would both allow easy evolutions of micromega with all exeutable code in the same repo (and overlays to test the theories on top of it) and easy adaptation of the user libraries, that would just have to peek the version they are using, while remaining compatible with multiple versions of Rocq.

[proux01]

Let's discuss that next week https://github.com/rocq-prover/rocq/wiki/Rocq-Call-2025-10-07

[andres-erbsen]

Having the definitions separate from the proofs does not seem acceptable to me, for all the reasons discussed during last call. Having micromega in its own repo could be discussed, but that repo would have to include or depend on the relevant stdlib proofs.

[proux01]

As written above, a micromega repo can't depend on Stdlib, it's the other way around: Stdlib depends on the micromega repo (so that Stdlib can choose its version of micromega).