diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked
index 1d9ec64b..23e66338 100644
--- a/.github/coq-concert.opam.locked
+++ b/.github/coq-concert.opam.locked
@@ -12,26 +12,19 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 depends: [
   "coq" {= "8.20.0"}
   "coq-bignums" {= "9.0.0+coq8.20"}
-  "coq-metacoq-common" {= "1.3.2+8.20"}
-  "coq-metacoq-erasure" {= "1.3.2+8.20"}
-  "coq-metacoq-pcuic" {= "1.3.2+8.20"}
-  "coq-metacoq-safechecker" {= "1.3.2+8.20"}
-  "coq-metacoq-template" {= "1.3.2+8.20"}
-  "coq-metacoq-template-pcuic" {= "1.3.2+8.20"}
-  "coq-metacoq-utils" {= "1.3.2+8.20"}
+  "coq-metacoq-common" {= "1.3.4+8.20"}
+  "coq-metacoq-erasure" {= "1.3.4+8.20"}
+  "coq-metacoq-pcuic" {= "1.3.4+8.20"}
+  "coq-metacoq-safechecker" {= "1.3.4+8.20"}
+  "coq-metacoq-template" {= "1.3.4+8.20"}
+  "coq-metacoq-template-pcuic" {= "1.3.4+8.20"}
+  "coq-metacoq-utils" {= "1.3.4+8.20"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "0.1.0"}
   "coq-quickchick" {= "2.0.4"}
   "coq-stdpp" {= "1.11.0"}
 ]
 pin-depends: [
-  ["coq-metacoq-utils.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-common.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-template.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-template-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-safechecker.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-erasure.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
   ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#c5d9cbae417213fe25b42f08678f28507cc6b99e"]
 ]
 build: [
diff --git a/.github/workflows/nix-action-8.20.yml b/.github/workflows/nix-action-8.20.yml
index 48f7e8bf..51cc0d54 100644
--- a/.github/workflows/nix-action-8.20.yml
+++ b/.github/workflows/nix-action-8.20.yml
@@ -45,15 +45,15 @@ jobs:
     - id: stepGetDerivation
       name: Getting derivation for current job (ConCert)
       run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.20\" --argstr job \"ConCert\" \\\n   --dry-run &> out || (touch
+        \"8.20\" --argstr job \"ConCert\" \\\n   --dry-run 2> err > out || (touch
         fail; true)\n"
     - name: Error reporting
-      run: "echo \"out=\"; cat out\n"
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
     - name: Failure check
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -128,15 +128,15 @@ jobs:
     - id: stepGetDerivation
       name: Getting derivation for current job (ElmExtraction)
       run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.20\" --argstr job \"ElmExtraction\" \\\n   --dry-run &> out || (touch
+        \"8.20\" --argstr job \"ElmExtraction\" \\\n   --dry-run 2> err > out || (touch
         fail; true)\n"
     - name: Error reporting
-      run: "echo \"out=\"; cat out\n"
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
     - name: Failure check
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -190,15 +190,15 @@ jobs:
     - id: stepGetDerivation
       name: Getting derivation for current job (QuickChick)
       run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.20\" --argstr job \"QuickChick\" \\\n   --dry-run &> out || (touch
+        \"8.20\" --argstr job \"QuickChick\" \\\n   --dry-run 2> err > out || (touch
         fail; true)\n"
     - name: Error reporting
-      run: "echo \"out=\"; cat out\n"
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
     - name: Failure check
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -261,15 +261,15 @@ jobs:
     - id: stepGetDerivation
       name: Getting derivation for current job (RustExtraction)
       run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.20\" --argstr job \"RustExtraction\" \\\n   --dry-run &> out ||
+        \"8.20\" --argstr job \"RustExtraction\" \\\n   --dry-run 2> err > out ||
         (touch fail; true)\n"
     - name: Error reporting
-      run: "echo \"out=\"; cat out\n"
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
     - name: Failure check
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -322,15 +322,15 @@ jobs:
     - id: stepGetDerivation
       name: Getting derivation for current job (coq)
       run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.20\" --argstr job \"coq\" \\\n   --dry-run &> out || (touch fail;
+        \"8.20\" --argstr job \"coq\" \\\n   --dry-run 2> err > out || (touch fail;
         true)\n"
     - name: Error reporting
-      run: "echo \"out=\"; cat out\n"
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
     - name: Failure check
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -376,15 +376,15 @@ jobs:
     - id: stepGetDerivation
       name: Getting derivation for current job (metacoq)
       run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.20\" --argstr job \"metacoq\" \\\n   --dry-run &> out || (touch
+        \"8.20\" --argstr job \"metacoq\" \\\n   --dry-run 2> err > out || (touch
         fail; true)\n"
     - name: Error reporting
-      run: "echo \"out=\"; cat out\n"
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
     - name: Failure check
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -454,15 +454,15 @@ jobs:
     - id: stepGetDerivation
       name: Getting derivation for current job (stdpp)
       run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.20\" --argstr job \"stdpp\" \\\n   --dry-run &> out || (touch fail;
+        \"8.20\" --argstr job \"stdpp\" \\\n   --dry-run 2> err > out || (touch fail;
         true)\n"
     - name: Error reporting
-      run: "echo \"out=\"; cat out\n"
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
     - name: Failure check
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -497,6 +497,3 @@ on:
   push:
     branches:
     - master
-concurrency:
-  group: "${{ github.workflow }}-${{ github.event.pull_request.number || github.head_ref || github.ref }}"
-  cancel-in-progress: true
diff --git a/.nix/config.nix b/.nix/config.nix
index aad4d8bf..adcac7fd 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -10,10 +10,10 @@
 
   bundles."8.20" = {
     coqPackages.coq.override.version = "8.20";
-    coqPackages.metacoq.override.version = "coq-8.20";
+    coqPackages.metacoq.override.version = "1.3.4-8.20";
     coqPackages.stdpp.override.version = "1.11.0";
     coqPackages.QuickChick.override.version = "2.0.4";
-    coqPackages.RustExtraction.override.version = "coq-8.20";
+    coqPackages.RustExtraction.override.version = "c5d9cbae417213fe25b42f08678f28507cc6b99e";
     coqPackages.ElmExtraction.override.version = "0.1.0";
   };
 
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
index 6062e55a..7332fcfa 100644
--- a/.nix/coq-nix-toolbox.nix
+++ b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"78d95509824be9e3339c1c0ee19f9c085f32b23e"
+"a1f630a232a3e2c739df99d0a947bf7465d2f8bb"
diff --git a/coq-concert.opam b/coq-concert.opam
index 4f942852..a687a36e 100644
--- a/coq-concert.opam
+++ b/coq-concert.opam
@@ -17,26 +17,19 @@ depends: [
   "coq" {>= "8.20" & < "8.21~"}
   "coq-bignums" {>= "8"}
   "coq-quickchick" {>= "2.0.4"}
-  "coq-metacoq-utils" {>= "1.3.1" & < "1.4~"}
-  "coq-metacoq-common" {>= "1.3.1" & < "1.4~"}
-  "coq-metacoq-template" {>= "1.3.1" & < "1.4~"}
-  "coq-metacoq-template-pcuic" {>= "1.3.1" & < "1.4~"}
-  "coq-metacoq-pcuic" {>= "1.3.1" & < "1.4~"}
-  "coq-metacoq-safechecker" {>= "1.3.1" & < "1.4~"}
-  "coq-metacoq-erasure" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-utils" {>= "1.3.4" & < "1.4~"}
+  "coq-metacoq-common" {>= "1.3.4" & < "1.4~"}
+  "coq-metacoq-template" {>= "1.3.4" & < "1.4~"}
+  "coq-metacoq-template-pcuic" {>= "1.3.4" & < "1.4~"}
+  "coq-metacoq-pcuic" {>= "1.3.4" & < "1.4~"}
+  "coq-metacoq-safechecker" {>= "1.3.4" & < "1.4~"}
+  "coq-metacoq-erasure" {>= "1.3.4" & < "1.4~"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "0.1.0"}
   "coq-stdpp" {>= "1.10.0" & < "1.12~"}
 ]
 
 pin-depends: [
-  ["coq-metacoq-utils.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-common.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-template.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-template-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-pcuic.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-safechecker.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
-  ["coq-metacoq-erasure.1.3.2+8.20" "git+https://github.com/MetaCoq/metacoq.git#ea3ed3c4b0d05508ce744f17a56c880c5f47c816"]
   ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#c5d9cbae417213fe25b42f08678f28507cc6b99e"]
 ]