diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index 32da72c78f..3bba7dc911 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -25,9 +25,10 @@ jobs:
           - coq-vst
           - coq-vst-32
     steps:
-      - uses: actions/checkout@v2
-      - name: Checkout submodules
-        uses: textbook/git-checkout-submodule-action@2.1.1
+      - name: Checkout
+        uses: actions/checkout@v2
+        with:
+          submodules: recursive
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: ${{ matrix.opam_name }}.opam
diff --git a/coq-vst-32.opam b/coq-vst-32.opam
index af7a25c3d4..d276dd77f7 100644
--- a/coq-vst-32.opam
+++ b/coq-vst-32.opam
@@ -17,16 +17,16 @@ dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
 bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
 license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE"
 build: [
-  [make "BITSIZE=32" "depend"]
-  [make "BITSIZE=32" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
+  [make "COMPCERT=bundled" "BITSIZE=32" "depend"]
+  [make "COMPCERT=bundled" "BITSIZE=32" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
 ]
-run-test: [make "BITSIZE=32" "-j%{jobs}%" "progs" "sha-hmac" "mailbox"]
+run-test: [make "COMPCERT=bundled" "BITSIZE=32" "-j%{jobs}%" "progs" "sha-hmac" "mailbox"]
 install: [
-	make "BITSIZE=32" "install"
+        make "COMPCERT=bundled" "BITSIZE=32" "install"
 	]
 depends: [
   "coq" {>= "8.11.0"}
-  "coq-compcert-32" {= "3.9"}
+  "coq-flocq" {>= "3.1.0" & < "4.0.0"} | "coq-flocq3" { = "dev"}
 ]
 synopsis: "Verified Software Toolchain"
 description:
diff --git a/coq-vst.opam b/coq-vst.opam
index c29a9a449e..7f0d882ca9 100644
--- a/coq-vst.opam
+++ b/coq-vst.opam
@@ -17,16 +17,16 @@ dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
 bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
 license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE"
 build: [
-  [make "BITSIZE=64" "depend"]
-  [make "BITSIZE=64" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
+  [make "COMPCERT=bundled" "BITSIZE=64" "depend"]
+  [make "COMPCERT=bundled" "BITSIZE=64" "-j%{jobs}%" "msl" "sepcomp" "veric" "floyd"]
 ]
-run-test: [make "BITSIZE=64" "-j%{jobs}%" "progs"]
+run-test: [make "COMPCERT=bundled" "BITSIZE=64" "-j%{jobs}%" "progs"]
 install: [
-	make "BITSIZE=64" "install"
+        make "COMPCERT=bundled" "BITSIZE=64" "install"
 	]
 depends: [
   "coq" {>= "8.11.0"}
-  "coq-compcert" {= "3.9"}
+  "coq-flocq" {>= "3.1.0" & < "4.0.0"} | "coq-flocq3" { = "dev"}
 ]
 synopsis: "Verified Software Toolchain"
 description: