diff --git a/.github/workflows/nix-action-default.yml b/.github/workflows/nix-action-default.yml
new file mode 100644
index 0000000..aa94505
--- /dev/null
+++ b/.github/workflows/nix-action-default.yml
@@ -0,0 +1,155 @@
+jobs:
+  coq:
+    needs: []
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which ref to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_ref=${{\
+        \ github.ref }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  if [ -z \"$merge_commit\" ]; then\n    echo \"tested_ref=refs/pull/${{\
+        \ github.event.number }}/head\" >> $GITHUB_ENV\n  else\n    echo \"tested_ref=refs/pull/${{\
+        \ github.event.number }}/merge\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_ref }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        name: coq
+    - name: Cachix setup coq-community
+      uses: cachix/cachix-action@v8
+      with:
+        name: coq-community
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        name: math-comp
+    - id: stepCheck
+      name: Checking presence of CI target coq
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"default\" --argstr job \"coq\" \\\n   --dry-run 2>&1 > /dev/null)\n\
+        echo ::set-output name=status::$(echo $nb_dry_run | grep \"built:\" | sed\
+        \ \"s/.*/built/\")\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 "default"
+        --argstr job "coq"
+  coqeal:
+    needs:
+    - coq
+    - paramcoq
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which ref to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_ref=${{\
+        \ github.ref }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  if [ -z \"$merge_commit\" ]; then\n    echo \"tested_ref=refs/pull/${{\
+        \ github.event.number }}/head\" >> $GITHUB_ENV\n  else\n    echo \"tested_ref=refs/pull/${{\
+        \ github.event.number }}/merge\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_ref }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        name: coq
+    - name: Cachix setup coq-community
+      uses: cachix/cachix-action@v8
+      with:
+        name: coq-community
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        name: math-comp
+    - id: stepCheck
+      name: Checking presence of CI target coqeal
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"default\" --argstr job \"coqeal\" \\\n   --dry-run 2>&1 > /dev/null)\n\
+        echo ::set-output name=status::$(echo $nb_dry_run | grep \"built:\" | sed\
+        \ \"s/.*/built/\")\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 "default"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: paramcoq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "paramcoq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "coqeal"
+  paramcoq:
+    needs:
+    - coq
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which ref to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_ref=${{\
+        \ github.ref }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  if [ -z \"$merge_commit\" ]; then\n    echo \"tested_ref=refs/pull/${{\
+        \ github.event.number }}/head\" >> $GITHUB_ENV\n  else\n    echo \"tested_ref=refs/pull/${{\
+        \ github.event.number }}/merge\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_ref }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        name: coq
+    - name: Cachix setup coq-community
+      uses: cachix/cachix-action@v8
+      with:
+        name: coq-community
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        name: math-comp
+    - id: stepCheck
+      name: Checking presence of CI target paramcoq
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"default\" --argstr job \"paramcoq\" \\\n   --dry-run 2>&1 > /dev/null)\n\
+        echo ::set-output name=status::$(echo $nb_dry_run | grep \"built:\" | sed\
+        \ \"s/.*/built/\")\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 "default"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "paramcoq"
+name: Nix CI for bundle default
+'on':
+  pull_request:
+    paths:
+    - .github/workflows/**
+  pull_request_target:
+    types:
+    - opened
+    - synchronize
+    - reopened
+  push:
+    branches:
+    - master
diff --git a/.nix/config.nix b/.nix/config.nix
new file mode 100644
index 0000000..5700f0e
--- /dev/null
+++ b/.nix/config.nix
@@ -0,0 +1,102 @@
+{
+  ## DO NOT CHANGE THIS
+  format = "1.0.0";
+  ## unless you made an automated or manual update
+  ## to another supported format.
+
+  ## The attribute to build from the local sources,
+  ## either using nixpkgs data or the overlays located in `.nix/coq-overlays`
+  ## Will determine the default main-job of the bundles defined below
+  attribute = "paramcoq";
+
+  ## If you want to select a different attribute (to build from the local sources as well)
+  ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument
+  # shell-attribute = "{{nix_name}}";
+
+  ## Maybe the shortname of the library is different from
+  ## the name of the nixpkgs attribute, if so, set it here:
+  # pname = "{{shortname}}";
+
+  ## Lists the dependencies, phrased in terms of nix attributes.
+  ## No need to list Coq, it is already included.
+  ## These dependencies will systematically be added to the currently
+  ## known dependencies, if any more than Coq.
+  ## /!\ Remove this field as soon as the package is available on nixpkgs.
+  ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then.
+  # buildInputs = [ ];
+
+  ## Indicate the relative location of your _CoqProject
+  ## If not specified, it defaults to "_CoqProject"
+  # coqproject = "_CoqProject";
+
+  ## select an entry to build in the following `bundles` set
+  ## defaults to "default"
+  default-bundle = "default";
+
+  ## write one `bundles.name` attribute set per
+  ## alternative configuration
+  ## When generating GitHub Action CI, one workflow file
+  ## will be created per bundle
+  bundles.default = {
+
+    ## You can override Coq and other Coq coqPackages
+    ## through the following attribute
+    coqPackages.coq.override.version = "master";
+    coqPackages.coqeal.override.version = "master";
+
+    ## In some cases, light overrides are not available/enough
+    ## in which case you can use either
+    # coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;
+    ## or a "long" overlay to put in `.nix/coq-overlays
+    ## you may use `nix-shell --run fetchOverlay <coq-pkg>`
+    ## to automatically retrieve the one from nixpkgs
+    ## if it exists and is correctly named/located
+
+    ## You can override Coq and other coqPackages
+    ## through the following attribute
+    ## If <ocaml-pkg> does not support light overrides,
+    ## you may use `overrideAttrs` or long overlays
+    ## located in `.nix/ocaml-overlays`
+    ## (there is no automation for this one)
+    #  ocamlPackages.<ocaml-pkg>.override.version = "x.xx";
+
+    ## You can also override packages from the nixpkgs toplevel
+    # <nix-pkg>.override.overrideAttrs = o: <overrides>;
+    ## Or put an overlay in `.nix/overlays`
+
+    ## you may mark a package as a main CI job (one to take deps and
+    ## rev deps from) as follows
+    # coqPackages.<main-pkg>.main-job = true;
+    ## by default the current package and its shell attributes are main jobs
+
+    ## you may mark a package as a CI job as follows
+    #  coqPackages.<another-pkg>.job = "test";
+    ## It can then built through
+    ## nix-build --argstr bundle "default" --arg job "test";
+    ## in the absence of such a directive, the job "another-pkg" will
+    ## is still available, but will be automatically included in the CI
+    ## via the command genNixActions only if it is a dependency or a
+    ## reverse dependency of a job flagged as "main-job" (see above).
+
+  };
+
+  ## Cachix caches to use in CI
+  ## Below we list some standard ones
+  cachix.coq = {};
+  cachix.math-comp = {};
+  cachix.coq-community = {};
+  
+  ## If you have write access to one of these caches you can
+  ## provide the auth token or signing key through a secret
+  ## variable on GitHub. Then, you should give the variable
+  ## name here. For instance, coq-community projects can use
+  ## the following line instead of the one above:
+  # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN";
+  
+  ## Or if you have a signing key for a given Cachix cache:
+  # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
+  
+  ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
+  ## are the names of secret variables. They are set in
+  ## GitHub's web interface.
+}
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
new file mode 100644
index 0000000..a8c436c
--- /dev/null
+++ b/.nix/coq-nix-toolbox.nix
@@ -0,0 +1 @@
+"4d8cc4ac0ce259be956939f80b3d57c94971a83f"
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000..1a24d7a
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,12 @@
+{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
+  update-nixpkgs ? false, ci-matrix ? false,
+  override ? {}, ocaml-override ? {}, global-override ? {},
+  bundle ? null, job ? null, inNixShell ? null, src ? ./.,
+}@args:
+let auto = fetchGit {
+  url = "https://github.com/coq-community/coq-nix-toolbox.git";
+  ref = "master";
+  rev = import .nix/coq-nix-toolbox.nix;
+};
+in
+import auto ({inherit src;} // args)