Prepare move of ring/field and micromega computational part to Corelib

.nix/config.nix

@@ -224,14 +224,18 @@ with builtins; with (import <nixpkgs> {}).lib;
       "metacoq-translations"
       "metacoq-utils"
       "metarocq"
+      "metarocq-common"
       "metarocq-erasure"
       "metarocq-erasure-plugin"
       "metarocq-pcuic"
       "metarocq-quotation"
       "metarocq-safechecker"
       "metarocq-safechecker-plugin"
       "metarocq-template-pcuic"
+      "metarocq-template-rocq"
       "metarocq-test"
+      "metarocq-translations"
+      "metarocq-utils"
       "rewriter"
       "riscvcoq"
       "rupicola"
@@ -265,6 +269,10 @@ with builtins; with (import <nixpkgs> {}).lib;
       #   for a complete list of Coq packages available in Nix
       # * <github_login>:<branch> is such that this will use the branch <branch>
       #   from https://github.com/<github_login>/<repository>
+      smtcoq.override.version = "proux01:stdlib207";
+      metarocq.override.version = "proux01:stdlib207";
+      metarocq-test.override.version = "proux01:stdlib207";
+      mathcomp-algebra-tactics.override.version = "proux01:stdlib207";
       sf.job = false;  # temporarily disactivated in Rocq CI
       trakt.job = false;  # temporarily disactivated in Rocq CI
       smtcoq-trakt.job = false;  # temporarily disactivated in Rocq CI
@@ -303,15 +311,13 @@ with builtins; with (import <nixpkgs> {}).lib;
       equations.override.version = "2137c8e7081f2d47ab903de0cc09fd6a05bfab01";
       equations-test.job = false;
       fiat-parsers.job = false;  # broken
-      metarocq.override.version = "2995003b88f3812e5649cfdd0f9a4c44ceaf0700";
-      metarocq-test.override.version = "2995003b88f3812e5649cfdd0f9a4c44ceaf0700";
       mtac2.override.version = "bcbefa79406fc113f878eb5f89758de241d81433";
       paramcoq-test.override.version = "937537d416bc5f7b81937d4223d7783d0e687239";
       perennial.job = false;  # broken
       relation-algebra.override.version = "4db15229396abfd8913685be5ffda4f0fdb593d9";
       rewriter.override.version = "9496defb8b236f442d11372f6e0b5e48aa38acfc";
       rocq-lean-import.override.version = "c3546102f242aaa1e9af921c78bdb1132522e444";
-      smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
+      # smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
       # smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
       stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
       unicoq.override.version = "28ec18aef35877829535316fc09825a25be8edf1";
@@ -341,13 +347,12 @@ with builtins; with (import <nixpkgs> {}).lib;
       equations.override.version = "1.3.1+9.0";
       equations-test.job = false;
       fiat-parsers.job = false;  # broken
-      metarocq.override.version = "1.4-9.0";
       mtac2.override.version = "1cdb2cb628444ffe9abc6535f6d2e11004de7fc1";
       paramcoq-test.override.version = "32609ca4a9bf4a0e456a855ea5118d8c00cda6be";
       perennial.job = false;  # broken
       relation-algebra.override.version = "7966d1a7bb524444120c56c3474717bcc91a5215";
       rocq-lean-import.override.version = "c513cee4f5edf8e8a06ba553ca58de5142cffde6";
-      smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
+      # smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
       # smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
       stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
       unicoq.override.version = "a9b72f755539c0b3280e38e778a09e2b7519a51a";

subcomponents/corelib_wrapper.v

@@ -3,6 +3,7 @@ From Stdlib Require Array.PrimArray.
 From Stdlib Require BinNums.IntDef.
 From Stdlib Require BinNums.NatDef.
 From Stdlib Require BinNums.PosDef.
+From Stdlib Require BinNums.RatDef.
 From Stdlib Require Classes.CMorphisms.
 From Stdlib Require Classes.CRelationClasses.
 From Stdlib Require Classes.Equivalence.

subcomponents/field.v

@@ -1,2 +1,3 @@
 From subcomponents Require zarith.
 From Stdlib Require setoid_ring.Field.
+From Stdlib Require setoid_ring.field_eval.

subcomponents/ring.v

@@ -21,4 +21,5 @@ From Stdlib Require setoid_ring.Ring_tac.
 From Stdlib Require setoid_ring.ArithRing.
 From Stdlib Require setoid_ring.NArithRing.
 From Stdlib Require setoid_ring.Ring_theory.
+From Stdlib Require setoid_ring.ring_eval.
 From Stdlib Require nsatz.NsatzTactic.