diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index fb75a9dc6097..2c785472114a 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -22,6 +22,7 @@ let
    "8.7.0"     = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m";
    "8.7.1"     = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8";
    "8.7.2"     = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w";
+   "8.8+beta1" = "19ipmx6bf8wjpk8y29hcginxk7hps4jh1bbihn5icx4qysm81165";
   }."${version}";
   coq-version = builtins.substring 0 3 version;
   camlp5 = ocamlPackages.camlp5_strict;
@@ -37,7 +38,7 @@ self = stdenv.mkDerivation {
   inherit camlp5;
   inherit (ocamlPackages) ocaml;
   passthru = {
-    inherit (ocamlPackages) findlib;
+    inherit (ocamlPackages) findlib num;
     emacsBufferSetup = pkgs: ''
       ; Propagate coq paths to children
       (inherit-local-permanent coq-prog-name "${self}/bin/coqtop")
@@ -92,7 +93,7 @@ self = stdenv.mkDerivation {
   };
 
   nativeBuildInputs = [ pkgconfig ];
-  buildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib camlp5 ncurses ]
+  buildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib camlp5 ncurses ocamlPackages.num ]
   ++ stdenv.lib.optional buildIde ocamlPackages.lablgtk;
 
   postPatch = ''
@@ -116,7 +117,6 @@ self = stdenv.mkDerivation {
 
   preConfigure = ''
     configureFlagsArray=(
-      -opt
       ${ideFlags}
     )
   '';
diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix
index 3f5ec69235f8..82c6e58a7b03 100644
--- a/pkgs/development/coq-modules/CoLoR/default.nix
+++ b/pkgs/development/coq-modules/CoLoR/default.nix
@@ -23,6 +23,6 @@ stdenv.mkDerivation {
   };
 
   passthru = {
-    compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6";
+    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ];
   };
 }
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index 72603ad44857..35cf63af8627 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -1,6 +1,6 @@
 { stdenv, fetchFromGitHub, coq, ssreflect }:
 
-let param =
+let params =
   {
     "8.5" = {
       version = "20170512";
@@ -19,9 +19,9 @@ let param =
       rev = "195e550a1cf0810497734356437a1720ebb6d744";
       sha256 = "0zm23y89z0h4iamy74qk9qi2pz2cj3ga6ygav0w79n0qyqwhxcq1";
     };
-
-  }."${coq.coq-version}"
-; in
+  };
+  param = params."${coq.coq-version}";
+in
 
 stdenv.mkDerivation rec {
 
@@ -49,4 +49,8 @@ stdenv.mkDerivation rec {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.hasAttr v params;
+  };
+
 }
diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix
index a27a247c9d0b..75e78d8ac44f 100644
--- a/pkgs/development/coq-modules/autosubst/default.nix
+++ b/pkgs/development/coq-modules/autosubst/default.nix
@@ -24,4 +24,6 @@ stdenv.mkDerivation rec {
     platforms = coq.meta.platforms;
   };
 
+  passthru = { inherit (mathcomp) compatibleCoqVersions; };
+
 }
diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index 9d035fec9f96..45786c5a9550 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -10,6 +10,10 @@ let param =
       rev = "V8.7.0";
       sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
     };
+    "8.8" = {
+      rev = "V8.8+beta1";
+      sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
+    };
   }."${coq.coq-version}"
 ; in
 
diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix
index 374979f1d15b..877331383a7d 100644
--- a/pkgs/development/coq-modules/coq-ext-lib/default.nix
+++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix
@@ -1,11 +1,12 @@
 { stdenv, fetchFromGitHub, coq }:
 
-let param =
+let params =
   {
     "8.5" = { version = "0.9.4"; sha256 = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; };
     "8.6" = { version = "0.9.5"; sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; };
     "8.7" = { version = "0.9.5"; sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; };
-  }."${coq.coq-version}";
+  };
+  param = params."${coq.coq-version}";
 in
 
 stdenv.mkDerivation rec {
@@ -34,4 +35,7 @@ stdenv.mkDerivation rec {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.hasAttr v params;
+  };
 }
diff --git a/pkgs/development/coq-modules/coq-haskell/default.nix b/pkgs/development/coq-modules/coq-haskell/default.nix
index b27fbcc15872..a66e941a8c9c 100644
--- a/pkgs/development/coq-modules/coq-haskell/default.nix
+++ b/pkgs/development/coq-modules/coq-haskell/default.nix
@@ -1,6 +1,6 @@
 { stdenv, fetchgit, coq, ssreflect }:
 
-let param =
+let params =
   {
     "8.5" = {
       version = "20171215";
@@ -19,9 +19,9 @@ let param =
       rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
       sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
     };
-
-  }."${coq.coq-version}"
-; in
+  };
+  param = params."${coq.coq-version}";
+in
 
 stdenv.mkDerivation rec {
 
@@ -48,4 +48,7 @@ stdenv.mkDerivation rec {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.hasAttr v params;
+  };
 }
diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix
index 7f5111462bd5..2e6c95bfe3c1 100644
--- a/pkgs/development/coq-modules/coquelicot/default.nix
+++ b/pkgs/development/coq-modules/coquelicot/default.nix
@@ -22,4 +22,7 @@ stdenv.mkDerivation {
     maintainers = [ stdenv.lib.maintainers.vbgl ];
     inherit (coq.meta) platforms;
   };
+
+  passthru = { inherit (ssreflect) compatibleCoqVersions; };
+
 }
diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix
index 425ab408c8c6..390ced8fdad3 100644
--- a/pkgs/development/coq-modules/dpdgraph/default.nix
+++ b/pkgs/development/coq-modules/dpdgraph/default.nix
@@ -1,6 +1,6 @@
 { stdenv, fetchFromGitHub, autoreconfHook, coq, ocamlPackages }:
 
-let param = {
+let params = {
   "8.7" = {
     version = "0.6.2";
     rev = "d76ddde37d918569945774733b7997e8b24daf51";
@@ -16,7 +16,9 @@ let param = {
     rev = "v0.6";
     sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
   };
-}."${coq.coq-version}"; in
+};
+param = params."${coq.coq-version}";
+in
 
 stdenv.mkDerivation {
   name = "coq${coq.coq-version}-dpdgraph-${param.version}";
@@ -46,4 +48,9 @@ stdenv.mkDerivation {
     maintainers = with stdenv.lib.maintainers; [ vbgl ];
     platforms = coq.meta.platforms;
   };
+
+  passthru = {
+    compatibleCoqVersions = v: builtins.hasAttr v params;
+  };
+
 }
diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/coq-modules/heq/default.nix
index 5f31fe6dc341..bf441562b14e 100644
--- a/pkgs/development/coq-modules/heq/default.nix
+++ b/pkgs/development/coq-modules/heq/default.nix
@@ -24,4 +24,7 @@ stdenv.mkDerivation rec {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: !stdenv.lib.versionAtLeast v "8.8";
+  };
 }
diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix
index 5faf8093b153..b1036e61f1bb 100644
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@@ -24,4 +24,7 @@ stdenv.mkDerivation {
     maintainers = with maintainers; [ vbgl ];
     platforms = coq.meta.platforms;
   };
+
+  passthru = { inherit (mathcomp) compatibleCoqVersions; };
+
 }
diff --git a/pkgs/development/coq-modules/mathcomp/generic.nix b/pkgs/development/coq-modules/mathcomp/generic.nix
index 564cb6f65717..5d39f9b3b0c8 100644
--- a/pkgs/development/coq-modules/mathcomp/generic.nix
+++ b/pkgs/development/coq-modules/mathcomp/generic.nix
@@ -35,4 +35,8 @@ stdenv.mkDerivation {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
+  };
+
 }
diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix
index 93ef7c14f1f3..94a24eb70858 100644
--- a/pkgs/development/coq-modules/paco/default.nix
+++ b/pkgs/development/coq-modules/paco/default.nix
@@ -28,4 +28,8 @@ stdenv.mkDerivation rec {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
+  };
+
 }
diff --git a/pkgs/development/coq-modules/ssreflect/generic.nix b/pkgs/development/coq-modules/ssreflect/generic.nix
index c598345403db..ca20e17dd50e 100644
--- a/pkgs/development/coq-modules/ssreflect/generic.nix
+++ b/pkgs/development/coq-modules/ssreflect/generic.nix
@@ -42,4 +42,8 @@ stdenv.mkDerivation {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
+  };
+
 }
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 443c4df47ac3..1235b2fd8263 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -19808,8 +19808,8 @@ with pkgs;
 
   inherit (callPackage ./coq-packages.nix {})
     mkCoqPackages
-    coq_8_3 coq_8_4 coq_8_5 coq_8_6 coq_8_7
-    coqPackages_8_5 coqPackages_8_6 coqPackages_8_7
+    coq_8_3 coq_8_4 coq_8_5 coq_8_6 coq_8_7 coq_8_8
+    coqPackages_8_5 coqPackages_8_6 coqPackages_8_7 coqPackages_8_8
     coqPackages coq
   ;
 
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 419fc485dd01..43d6d8d2dd5e 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -71,10 +71,14 @@ in rec {
   coq_8_7 = callPackage ../applications/science/logic/coq {
     version = "8.7.2";
   };
+  coq_8_8 = callPackage ../applications/science/logic/coq {
+    version = "8.8+beta1";
+  };
 
   coqPackages_8_5 = mkCoqPackages coq_8_5;
   coqPackages_8_6 = mkCoqPackages coq_8_6;
   coqPackages_8_7 = mkCoqPackages coq_8_7;
+  coqPackages_8_8 = mkCoqPackages coq_8_8;
   coqPackages = coqPackages_8_7;
   coq = coqPackages.coq;