Abel-Galois for any characteristic

.nix/config.nix

@@ -31,7 +31,7 @@
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
-  default-bundle = "coq8.20+mcmathcomp-2.3.0";
+  default-bundle = "coq-9.0";
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration

.nix/coq-overlays/mathcomp-abel/default.nix

@@ -0,0 +1,27 @@
+{ coq, mkCoqDerivation, mathcomp, mathcomp-real-closed, lib, version ? null }:
+
+mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "abel";
+  owner = "math-comp";
+
+  inherit version;
+  defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ];           out = "1.2.0"; }
+      { cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; }
+    ] null;
+
+  release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";
+  release."1.1.2".sha256 = "0565w713z1cwxvvdlqws2z5lgdys8lddf0vpwfdj7bpd7pq9hwxg";
+  release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
+
+
+  propagatedBuildInputs = [ mathcomp.character mathcomp-real-closed ];
+
+  meta = with lib; {
+    description = "Abel - Galois and Abel - Ruffini Theorems";
+    license = licenses.cecill-b;
+    maintainers = [ maintainers.cohencyril ];
+  };
+}

_CoqProject

@@ -6,6 +6,7 @@ theories/xmathcomp/map_gal.v
 theories/xmathcomp/char0.v
 theories/xmathcomp/cyclotomic_ext.v
 theories/xmathcomp/real_closed_ext.v
+theories/xmathcomp/artin_scheier.v
 
 -R theories Abel
 -arg -w -arg -projection-no-head-constant
@@ -15,4 +16,4 @@ theories/xmathcomp/real_closed_ext.v
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +non-primitive-record
 -arg -w -arg +undeclared-scope
--arg -w -arg +implicit-core-hint-db
+-arg -w -arg +implicit-core-hint-db