diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index c769ab5521e8..d573eca809a2 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -3,6 +3,9 @@
 }:
 with builtins // stdenv.lib;
 let
+  ####################################
+  # CONFIGURATION (please edit this) #
+  ####################################
   # sha256 of released mathcomp versions
   mathcomp-sha256 = {
     "1.9.0" = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
@@ -19,8 +22,16 @@ let
   };
   # computes the default version of mathcomp given a version of Coq
   max-mathcomp-version = last (naturalSort (attrNames mathcomp-coq-versions));
-  default-mathcomp-version = let v = last (naturalSort (["0.0.0"]
-     ++ (attrNames (filterAttrs (_: vs: vs coq.coq-version) mathcomp-coq-versions))));
+  # mathcomp prefered version by decreasing order
+  # (the first version in the list will be tried first)
+  mathcomp-version-preference = [ "1.8.0" "1.9.0" "1.7.0" "1.6.1" ];
+
+  ##############################################################
+  # COMPUTED using the configuration above (edit with caution) #
+  ##############################################################
+  default-mathcomp-version = let v = head (
+    filter (mc: mathcomp-coq-versions."${mc}" coq.coq-version)
+            mathcomp-version-preference ++ ["0.0.0"]);
      in if v == "0.0.0" then max-mathcomp-version else v;
 
   # list of core mathcomp packages sorted by dependency order
diff --git a/pkgs/development/coq-modules/mathcomp/extra.nix b/pkgs/development/coq-modules/mathcomp/extra.nix
index c30ba19b75a3..0d9557623c36 100644
--- a/pkgs/development/coq-modules/mathcomp/extra.nix
+++ b/pkgs/development/coq-modules/mathcomp/extra.nix
@@ -1,7 +1,7 @@
-{ stdenv, fetchFromGitHub, coq, mathcomp, coqPackages,
+{ stdenv, fetchFromGitHub, coq, ssreflect, coqPackages,
   recurseIntoAttrs }:
 with builtins // stdenv.lib;
-let current-mathcomp = mathcomp; in
+let current-ssreflect = ssreflect; in
 let
 # configuring packages
 param = {
@@ -20,6 +20,7 @@ param = {
   };
   multinomials = {
     version-sha256 = {
+      "1.3" = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4";
       "1.2" = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
       "1.1" = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
       "1.0" = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
@@ -32,7 +33,9 @@ param = {
       "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
       "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al";
     };
+    compatibleCoqVersions = flip elem ["8.8" "8.9"];
     description = "Analysis library compatible with Mathematical Components";
+    license = stdenv.lib.licenses.cecill-c;
   };
   real-closed = {
     version-sha256 = {
@@ -42,6 +45,15 @@ param = {
     };
     description = "Mathematical Components Library on real closed fields";
   };
+  coqeal = {
+    version-sha256 = {
+      "1.0.0" = "1had6f1n85lmh9x31avbmgl3m0rsiw9f8ma95qzk5b57fjg5k1ii";
+    };
+    description = "CoqEAL - The Coq Effective Algebra Library";
+    owner = "CoqEAL";
+    compatibleCoqVersions = flip elem ["8.7" "8.8" "8.9"];
+    license = stdenv.lib.licenses.mit;
+  };
 };
 versions = {
   "1.9.0" = {
@@ -49,13 +61,17 @@ versions = {
     bigenough.version = "1.0.0";
     analysis = {
       version = "0.2.2";
-      core-deps = with coqPackages; [ mathcomp_1_9-field ];
+      core-deps = with coqPackages; [ mathcomp-field_1_9 ];
+      extra-deps = with coqPackages; [ mathcomp_1_9-finmap mathcomp_1_9-bigenough ];
+    };
+    multinomials = {
+      version = "1.3";
+      core-deps = with coqPackages; [ mathcomp-algebra_1_9 ];
       extra-deps = with coqPackages; [ mathcomp_1_9-finmap mathcomp_1_9-bigenough ];
     };
-    multinomials = {};
     real-closed = {
       version = "1.0.3";
-      core-deps = with coqPackages; [ mathcomp_1_9-field ];
+      core-deps = with coqPackages; [ mathcomp-field_1_9 ];
       extra-deps = with coqPackages; [ mathcomp_1_9-bigenough ];
     };
   }; 
@@ -64,37 +80,42 @@ versions = {
     bigenough.version = "1.0.0";
     analysis = {
       version = "0.2.2";
-      core-deps = with coqPackages; [ mathcomp_1_8-field ];
+      core-deps = with coqPackages; [ mathcomp-field_1_8 ];
       extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
     };
     multinomials = {
-      version = "1.2";
-      core-deps = with coqPackages; [ mathcomp_1_8-algebra ];
+      version = "1.3";
+      core-deps = with coqPackages; [ mathcomp-algebra_1_8 ];
       extra-deps = with coqPackages; [ mathcomp_1_8-finmap mathcomp_1_8-bigenough ];
     };
     real-closed = {
       version = "1.0.3";
-      core-deps = with coqPackages; [ mathcomp_1_8-field ];
+      core-deps = with coqPackages; [ mathcomp-field_1_8 ];
       extra-deps = with coqPackages; [ mathcomp_1_8-bigenough ];
     };
+    coqeal = {
+      version = "1.0.0";
+      core-deps = with coqPackages; [ mathcomp-algebra_1_8 ];
+      extra-deps = with coqPackages; [ bignums paramcoq mathcomp_1_8-multinomials ];
+    };
   };
   "1.7.0" = {
     finmap.version = "1.1.0";
     bigenough.version = "1.0.0";
     analysis = {
       version = "0.1.0";
-      core-deps = with coqPackages; [ mathcomp_1_7-field ];
+      core-deps = with coqPackages; [ mathcomp-field_1_7 ];
       extra-deps = with coqPackages; [ mathcomp_1_7-finmap mathcomp_1_7-bigenough ];
     };
     multinomials = {
       version = "1.1";
-      core-deps = with coqPackages; [ mathcomp_1_7-algebra ];
+      core-deps = with coqPackages; [ mathcomp-algebra_1_7 ];
       extra-deps = with coqPackages; [ mathcomp_1_7-finmap_1_0 mathcomp_1_7-bigenough ];
     };
     real-closed = {
       version = "1.0.1";
-      core-deps = with coqPackages; [ mathcomp_1_8-field ];
-      extra-deps = with coqPackages; [ mathcomp_1_8-bigenough ];
+      core-deps = with coqPackages; [ mathcomp-field_1_7 ];
+      extra-deps = with coqPackages; [ mathcomp_1_7-bigenough ];
     };
   };
 };
@@ -104,24 +125,25 @@ packageGen = {
   # optional arguments
   src ? "",
   owner ? "math-comp",
-  core-deps ? [ coqPackages.mathcomp-ssreflect ],
   extra-deps ? [],
-  mathcomp ? current-mathcomp,
+  ssreflect ? current-ssreflect,
+  core-deps ? null,
   compatibleCoqVersions ? null,
-  license ? mathcomp.meta.license,
+  license ? ssreflect.meta.license,
   # mandatory
   package, version ? "broken", version-sha256, description
   }:
   let
     theCompatibleCoqVersions = if compatibleCoqVersions == null
-                               then mathcomp.compatibleCoqVersions
+                               then ssreflect.compatibleCoqVersions
                                else compatibleCoqVersions;
+    mc-core-deps = if builtins.isNull core-deps then [ssreflect] else core-deps;
   in
   { "${package}" = let from = src; in
 
   stdenv.mkDerivation rec {
     inherit version;
-    name = "coq${coq.coq-version}-mathcomp-${mathcomp.version}-${package}-${version}";
+    name = "coq${coq.coq-version}-mathcomp${ssreflect.version}-${package}-${version}";
 
     src = if from == "" then fetchFromGitHub {
       owner = owner;
@@ -130,7 +152,7 @@ packageGen = {
       sha256 = version-sha256."${version}";
     } else from;
 
-    propagatedBuildInputs = [ coq mathcomp ] ++ extra-deps;
+    propagatedBuildInputs = [ coq ] ++ mc-core-deps ++ extra-deps;
 
     installFlags = "-f Makefile.coq COQLIB=$(out)/lib/coq/${coq.coq-version}/";
 
@@ -138,7 +160,7 @@ packageGen = {
       inherit description;
       inherit license;
       inherit (src.meta) homepage;
-      inherit (mathcomp.meta) platforms;
+      inherit (ssreflect.meta) platforms;
       maintainers = [ stdenv.lib.maintainers.vbgl ];
       broken = (version == "broken");
     };
@@ -151,14 +173,14 @@ packageGen = {
   };
   };
 
-current-versions = versions."${current-mathcomp.version}" or {};
+current-versions = versions."${current-ssreflect.version}" or {};
 
 select = x: mapAttrs (n: pkg: {package = n;} // pkg) (recursiveUpdate param x);
 
 for-version = v: suffix: (mapAttrs' (n: pkg:
         {name = "mathcomp_${suffix}-${n}";
          value = (packageGen ({
-             mathcomp = coqPackages."mathcomp_${suffix}";
+             ssreflect = coqPackages."mathcomp-ssreflect_${suffix}";
            } // pkg))."${n}";})
         (select versions."${v}"));
 
@@ -173,7 +195,8 @@ in
 mathcompExtraGen = packageGen;
 mathcomp_1_7-finmap_1_0 =
   (packageGen (select {finmap = {version = "1.0.0";
-                                 mathcomp = coqPackages.mathcomp_1_7;};
+                                 ssreflect = coqPackages.mathcomp-ssreflect_1_7;};
                       }).finmap).finmap;
 multinomials = all.mathcomp-multinomials;
+coqeal = all.mathcomp-coqeal;
 } // all
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 524f3bf43994..8a987c6cf143 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -54,17 +54,17 @@ let
         mathcomp-ssreflect_1_9 mathcomp-fingroup_1_9 mathcomp-algebra_1_9
         mathcomp-solvable_1_9 mathcomp-field_1_9 mathcomp-character_1_9;
       inherit (callPackage ../development/coq-modules/mathcomp/extra.nix { })
-        mathcompExtraGen multinomials
+        mathcompExtraGen multinomials coqeal
 
         mathcomp-finmap mathcomp-bigenough mathcomp-analysis
-        mathcomp-multinomials mathcomp-real-closed
+        mathcomp-multinomials mathcomp-real-closed mathcomp-coqeal
 
         mathcomp_1_7-finmap mathcomp_1_7-bigenough mathcomp_1_7-analysis
         mathcomp_1_7-multinomials mathcomp_1_7-real-closed
         mathcomp_1_7-finmap_1_0
 
         mathcomp_1_8-finmap mathcomp_1_8-bigenough mathcomp_1_8-analysis
-        mathcomp_1_8-multinomials mathcomp_1_8-real-closed
+        mathcomp_1_8-multinomials mathcomp_1_8-real-closed mathcomp_1_8-coqeal
 
         mathcomp_1_9-finmap mathcomp_1_9-bigenough mathcomp_1_9-analysis
         mathcomp_1_9-multinomials mathcomp_1_9-real-closed;