diff --git a/pkgs/development/compilers/compcert/default.nix b/pkgs/development/compilers/compcert/default.nix
index 3dea91970e2..99bd09d8d9e 100644
--- a/pkgs/development/compilers/compcert/default.nix
+++ b/pkgs/development/compilers/compcert/default.nix
@@ -1,36 +1,52 @@
-{ stdenv, lib, fetchFromGitHub, fetchpatch, makeWrapper
-, coq, ocamlPackages, coq2html
+{ stdenv, fetchFromGitHub, fetchpatch, makeWrapper
+, coqPackages, ocamlPackages, coq2html
 , tools ? stdenv.cc
+, version ? "3.8"
 }:
 
 let
   ocaml-pkgs      = with ocamlPackages; [ ocaml findlib menhir ];
   ccomp-platform = if stdenv.isDarwin then "x86_64-macosx" else "x86_64-linux";
+  inherit (coqPackages) coq flocq;
+  inherit (stdenv.lib) optional optionalString;
 in
+
+let param = {
+  "3.7" = {
+    sha256 = "1h4zhk9rrqki193nxs9vjvya7nl9yxjcf07hfqb6g77riy1vd2jr";
+    patches = [
+     (fetchpatch {
+        url = "https://github.com/AbsInt/CompCert/commit/0a2db0269809539ccc66f8ec73637c37fbd23580.patch";
+        sha256 = "0n8qrba70x8f422jdvq9ddgsx6avf2dkg892g4ldh3jiiidyhspy";
+      })
+     (fetchpatch {
+        url = "https://github.com/AbsInt/CompCert/commit/5e29f8b5ba9582ecf2a1d0baeaef195873640607.patch";
+        sha256 = "184nfdgxrkci880lkaj5pgnify3plka7xfgqrgv16275sqppc5hc";
+      })
+    ];
+  };
+  "3.8" = {
+    sha256 = "1gzlyxvw64ca12qql3wnq3bidcx9ygsklv9grjma3ib4hvg7vnr7";
+    useExternalFlocq = true;
+  };
+}."${version}"; in
+
 stdenv.mkDerivation rec {
   pname = "compcert";
-  version = "3.7";
+  inherit version;
 
   src = fetchFromGitHub {
     owner = "AbsInt";
     repo = "CompCert";
     rev = "v${version}";
-    sha256 = "1h4zhk9rrqki193nxs9vjvya7nl9yxjcf07hfqb6g77riy1vd2jr";
+    inherit (param) sha256;
   };
 
-  patches = [
-   (fetchpatch {
-      url = "https://github.com/AbsInt/CompCert/commit/0a2db0269809539ccc66f8ec73637c37fbd23580.patch";
-      sha256 = "0n8qrba70x8f422jdvq9ddgsx6avf2dkg892g4ldh3jiiidyhspy";
-    })
-   (fetchpatch {
-      url = "https://github.com/AbsInt/CompCert/commit/5e29f8b5ba9582ecf2a1d0baeaef195873640607.patch";
-      sha256 = "184nfdgxrkci880lkaj5pgnify3plka7xfgqrgv16275sqppc5hc";
-    })
-  ];
+  patches = param.patches or [];
 
   nativeBuildInputs = [ makeWrapper ];
   buildInputs = ocaml-pkgs ++ [ coq coq2html ];
+  propagatedBuildInputs = optional (param.useExternalFlocq or false) flocq;
   enableParallelBuilding = true;
 
   postPatch = ''
@@ -43,6 +59,7 @@ stdenv.mkDerivation rec {
       -prefix $out \
       -coqdevdir $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ \
       -toolprefix ${tools}/bin/ \
+      ${optionalString (param.useExternalFlocq or false) "-use-external-Flocq"} \
       ${ccomp-platform}
   '';
 
@@ -68,7 +85,7 @@ stdenv.mkDerivation rec {
 
   meta = with stdenv.lib; {
     description = "Formally verified C compiler";
-    homepage    = "http://compcert.inria.fr";
+    homepage    = "https://compcert.org";
     license     = licenses.inria-compcert;
     platforms   = [ "x86_64-linux" "x86_64-darwin" ];
     maintainers = with maintainers; [ thoughtpolice jwiegley vbgl ];
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 605db554363..46b7094cb3a 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -1,4 +1,6 @@
-{ lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09 }:
+{ lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
+, compcert
+}:
 
 let
   mkCoqPackages' = self: coq:
@@ -59,7 +61,9 @@ let
       tlc = callPackage ../development/coq-modules/tlc {};
       Velisarios = callPackage ../development/coq-modules/Velisarios {};
       Verdi = callPackage ../development/coq-modules/Verdi {};
-      VST = callPackage ../development/coq-modules/VST {};
+      VST = callPackage ../development/coq-modules/VST {
+        compcert = compcert.override { version = "3.7"; };
+      };
 
       filterPackages = filterCoqPackages;
     };