diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml
index e1ad3cd55..c8a140302 100644
--- a/.github/workflows/nix-action-coq-8.19.yml
+++ b/.github/workflows/nix-action-coq-8.19.yml
@@ -1,8 +1,6 @@
 jobs:
-  ElmExtraction:
-    needs:
-    - coq
-    - metacoq
+  coq:
+    needs: []
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -29,7 +27,7 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v30
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup coq
@@ -38,25 +36,18 @@ jobs:
         extraPullNames: coq-community
         name: coq
     - id: stepCheck
-      name: Checking presence of CI target ElmExtraction
+      name: Checking presence of CI target coq
       run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"coq-8.19\" --argstr job \"ElmExtraction\" \\\n   --dry-run 2>&1\
-        \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\
-        built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
-    - 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 "coq-8.19"
-        --argstr job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: metacoq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
-        --argstr job "metacoq"
+        \ bundle \"coq-8.19\" --argstr job \"coq\" \\\n   --dry-run 2>&1 > /dev/null)\n\
+        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
+        s/.*/built/\") >> $GITHUB_OUTPUT\n"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
-        --argstr job "ElmExtraction"
-  coq:
-    needs: []
+        --argstr job "coq"
+  equations:
+    needs:
+    - coq
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -83,7 +74,7 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v30
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup coq
@@ -92,18 +83,23 @@ jobs:
         extraPullNames: coq-community
         name: coq
     - id: stepCheck
-      name: Checking presence of CI target coq
+      name: Checking presence of CI target equations
       run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"coq-8.19\" --argstr job \"coq\" \\\n   --dry-run 2>&1 > /dev/null)\n\
+        \ bundle \"coq-8.19\" --argstr job \"equations\" \\\n   --dry-run 2>&1 > /dev/null)\n\
         echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
         s/.*/built/\") >> $GITHUB_OUTPUT\n"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
+      name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
         --argstr job "coq"
-  equations:
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "equations"
+  library-undecidability:
     needs:
     - coq
+    - metacoq
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -130,7 +126,7 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v30
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup coq
@@ -139,19 +135,23 @@ jobs:
         extraPullNames: coq-community
         name: coq
     - id: stepCheck
-      name: Checking presence of CI target equations
+      name: Checking presence of CI target library-undecidability
       run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
-        \ bundle \"coq-8.19\" --argstr job \"equations\" \\\n   --dry-run 2>&1 > /dev/null)\n\
-        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
-        s/.*/built/\") >> $GITHUB_OUTPUT\n"
+        \ bundle \"coq-8.19\" --argstr job \"library-undecidability\" \\\n   --dry-run\
+        \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
+        \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
     - 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 "coq-8.19"
         --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "metacoq"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
-        --argstr job "equations"
+        --argstr job "library-undecidability"
   metacoq:
     needs:
     - coq
@@ -182,7 +182,7 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v30
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup coq
diff --git a/.nix/config.nix b/.nix/config.nix
index 73ba74f7b..1f1110cba 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -46,7 +46,8 @@
     push-branches = ["coq-8.19"];
 
     # Reverse dependencies
-    coqPackages.ElmExtraction.override.version = "master";
+    # coqPackages.ElmExtraction.override.version = "master";
+    coqPackages.library-undecidability.override.version = "coq-8.19";
   };
 
   ## Cachix caches to use in CI
diff --git a/.nix/coq-overlays/library-undecidability/default.nix b/.nix/coq-overlays/library-undecidability/default.nix
new file mode 100644
index 000000000..595955e80
--- /dev/null
+++ b/.nix/coq-overlays/library-undecidability/default.nix
@@ -0,0 +1,59 @@
+## File initially generated by createOverlay
+## and then supposedly modified manually.
+## Some hints for manual modifications are in the file,
+## but the full doc is on nixos / nix packages website:
+## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq
+
+{ lib, mkCoqDerivation, which, coq
+  ## declare extra dependencies here, to be used in propagateBuildInputs e.g.
+  , metacoq
+  , version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "library-undecidability";
+  repo = "coq-library-undecidability";
+  owner = "uds-psl";
+  domain = "github.com";
+
+  inherit version;
+## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged
+## for local usage since it will be ignored locally if
+## - this derivation corresponds to the main attribute,
+## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`.
+  defaultVersion = with versions; switch coq.coq-version [
+    ## Example of possible dependencies
+    # { case = range "8.13" "8.14"; out = "1.2.0"; }
+    ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc
+  ] null;
+
+  ## Declare existing releases
+  ## leave sha256 empty at first and then copy paste
+  ## the resulting sha given by the error message
+  # release."1.1.1".sha256 = "";
+  ## if the tag is not exactly the version number you can amend like this
+  # release."1.1.1".rev = "v1.1.1";
+  ## if a consistent scheme gives the tag from the release number, you can do like this:
+  # releaseRev = v: "v${v}";
+
+  ## Add dependencies in here. In particular you can add
+  ## - arbitrary nix packages (you need to require them at the beginning of the file)
+  ## - Coq packages (require them at the beginning of the file)
+  ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file)
+  propagatedBuildInputs = [ metacoq ];
+
+  ## Does the package contain OCaml code?
+  # mlPlugin = false;
+
+  ## Give some meta data
+  ## This is needed for submitting the package to nixpkgs but not required for local use.
+  meta = {
+    ## Describe your package in one sentence
+    # description = "";
+    ## Kindly ask one of these people if they want to be an official maintainer.
+    ## (You might also consider adding yourself to the list of maintainers)
+    # maintainers = with maintainers; [ cohencyril siraben vbgl Zimmi48 ];
+    ## Pick a license from
+    ## https://github.com/NixOS/nixpkgs/blob/master/lib/licenses.nix
+    # license = licenses.mit;
+  };
+}