diff --git a/.github/workflows/flake-build.yml b/.github/workflows/flake-build.yml
new file mode 100644
index 00000000..12051774
--- /dev/null
+++ b/.github/workflows/flake-build.yml
@@ -0,0 +1,27 @@
+name: Flake build
+
+# Controls when the action will run.
+on:
+  # Triggers the workflow on push or pull request events but only for the main branch
+  push:
+    branches: [ main ]
+  pull_request:
+    branches: [ main ]
+
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+jobs:
+  # This workflow contains a single job called "build"
+  build:
+    # The type of runner that the job will run on
+    runs-on: ubuntu-latest
+
+    # Steps represent a sequence of tasks that will be executed as part of the job
+    steps:
+    - uses: actions/checkout@v4
+    - uses: cachix/install-nix-action@v25
+      with:
+        github_access_token: ${{ secrets.GITHUB_TOKEN }}
+    - run: nix build
+    - run: nix flake check
diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml
new file mode 100644
index 00000000..7857c760
--- /dev/null
+++ b/.github/workflows/nix-action-8.18.yml
@@ -0,0 +1,281 @@
+jobs:
+  coq:
+    needs: []
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v20
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v12
+      with:
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - 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 \"8.18\" --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 "8.18" --argstr
+        job "coq"
+  mathcomp:
+    needs:
+    - coq
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v20
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v12
+      with:
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - id: stepCheck
+      name: Checking presence of CI target mathcomp
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"8.18\" --argstr job \"mathcomp\" \\\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 previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-ssreflect"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-fingroup'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-fingroup"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-algebra'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-algebra"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-solvable'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-solvable"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-field'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-field"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-character'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-character"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: hierarchy-builder'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "hierarchy-builder"
+    - 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.18" --argstr
+        job "mathcomp"
+  mathcomp-analysis:
+    needs:
+    - coq
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v20
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v12
+      with:
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - id: stepCheck
+      name: Checking presence of CI target mathcomp-analysis
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"8.18\" --argstr job \"mathcomp-analysis\" \\\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 "8.18" --argstr
+        job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-classical'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-classical"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-field'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-field"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-bigenough'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-bigenough"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: hierarchy-builder'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "hierarchy-builder"
+    - 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.18" --argstr
+        job "mathcomp-analysis"
+  ssprove:
+    needs:
+    - coq
+    - mathcomp-analysis
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v20
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v12
+      with:
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - id: stepCheck
+      name: Checking presence of CI target ssprove
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"8.18\" --argstr job \"ssprove\" \\\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 previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: equations'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "equations"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-ssreflect"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-analysis'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "mathcomp-analysis"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: extructures'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "extructures"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: deriving'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
+        job "deriving"
+    - 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.18" --argstr
+        job "ssprove"
+name: Nix CI for bundle 8.18
+'on':
+  pull_request:
+    paths:
+    - .github/workflows/nix-action-8.18.yml
+  pull_request_target:
+    paths-ignore:
+    - .github/workflows/nix-action-8.18.yml
+    types:
+    - opened
+    - synchronize
+    - reopened
+  push:
+    branches:
+    - main
+  workflow_dispatch:
diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml
new file mode 100644
index 00000000..36cebd71
--- /dev/null
+++ b/.github/workflows/nix-action-8.19.yml
@@ -0,0 +1,281 @@
+jobs:
+  coq:
+    needs: []
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v20
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v12
+      with:
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - 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 \"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 "8.19" --argstr
+        job "coq"
+  mathcomp:
+    needs:
+    - coq
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v20
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v12
+      with:
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - id: stepCheck
+      name: Checking presence of CI target mathcomp
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"8.19\" --argstr job \"mathcomp\" \\\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 previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-ssreflect"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-fingroup'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-fingroup"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-algebra'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-algebra"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-solvable'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-solvable"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-field'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-field"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-character'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-character"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: hierarchy-builder'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "hierarchy-builder"
+    - 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.19" --argstr
+        job "mathcomp"
+  mathcomp-analysis:
+    needs:
+    - coq
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v20
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v12
+      with:
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - id: stepCheck
+      name: Checking presence of CI target mathcomp-analysis
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"8.19\" --argstr job \"mathcomp-analysis\" \\\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 "8.19" --argstr
+        job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-classical'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-classical"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-field'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-field"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-bigenough'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-bigenough"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: hierarchy-builder'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "hierarchy-builder"
+    - 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.19" --argstr
+        job "mathcomp-analysis"
+  ssprove:
+    needs:
+    - coq
+    - mathcomp-analysis
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v20
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v12
+      with:
+        extraPullNames: coq-community, math-comp
+        name: coq
+    - id: stepCheck
+      name: Checking presence of CI target ssprove
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"8.19\" --argstr job \"ssprove\" \\\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 previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: equations'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "equations"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-ssreflect"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: mathcomp-analysis'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "mathcomp-analysis"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: extructures'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "extructures"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: deriving'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
+        job "deriving"
+    - 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.19" --argstr
+        job "ssprove"
+name: Nix CI for bundle 8.19
+'on':
+  pull_request:
+    paths:
+    - .github/workflows/nix-action-8.19.yml
+  pull_request_target:
+    paths-ignore:
+    - .github/workflows/nix-action-8.19.yml
+    types:
+    - opened
+    - synchronize
+    - reopened
+  push:
+    branches:
+    - main
+  workflow_dispatch:
diff --git a/.github/workflows/build.yml b/.github/workflows/opam-build.yml
similarity index 98%
rename from .github/workflows/build.yml
rename to .github/workflows/opam-build.yml
index 46141271..46ca966a 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/opam-build.yml
@@ -1,6 +1,6 @@
 # This is a basic workflow to help you get started with Actions
 
-name: Test build
+name: Opam build
 
 # Controls when the action will run.
 on:
diff --git a/.nix/config.nix b/.nix/config.nix
new file mode 100644
index 00000000..195296dd
--- /dev/null
+++ b/.nix/config.nix
@@ -0,0 +1,81 @@
+{
+  ## 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 = "ssprove";
+
+  ## 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 = "8.19";
+
+  ## write one `bundles.name` attribute set per
+  ## alternative configuration
+  ## When generating GitHub Action CI, one workflow file
+  ## will be created per bundle
+
+  ## It is not possible as of yet to the coq-nix-toolbox to use a
+  ## certain version. All jobs only run against the latest version.
+  ## To do this check as a CI job you either need to manually edit
+  ## the generated workflow or create branch off of version 0.1.0
+  ## and add it there.
+ # bundles."8.17".coqPackages = {
+ #   coq.override.version = "8.17";
+ #   mathcomp.override.version = "1.17.0";
+ #   mathcomp-analysis.override.version = "0.6.0";
+ # };
+  bundles."8.18".coqPackages = {
+    coq.override.version = "8.18";
+    mathcomp.override.version = "2.1.0";
+    mathcomp-analysis.override.version = "1.0.0";
+  };
+  bundles."8.19".coqPackages = {
+    coq.override.version = "8.19";
+    mathcomp.override.version = "2.2.0";
+    mathcomp-analysis.override.version = "1.0.0";
+  };
+
+  ## 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 00000000..c3398402
--- /dev/null
+++ b/.nix/coq-nix-toolbox.nix
@@ -0,0 +1 @@
+"544d3d77a4a0f4fef30ad7825d2a8d2255abb0e3"
diff --git a/.nix/flake.nix.template_latest b/.nix/flake.nix.template_latest
new file mode 100644
index 00000000..73098e95
--- /dev/null
+++ b/.nix/flake.nix.template_latest
@@ -0,0 +1,22 @@
+{
+  inputs = {
+    nixpkgs.url        = github:nixos/nixpkgs;
+    flake-utils.url    = github:numtide/flake-utils;
+
+    ssprove.url = github:ssprove/ssprove/nix;
+    ssprove.inputs.nixpkgs.follows = "nixpkgs";
+    ssprove.inputs.flake-utils.follows = "flake-utils";
+ };
+  outputs = { self, nixpkgs, flake-utils
+            , ssprove }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let
+        pkgs = nixpkgs.legacyPackages.${system};
+      in {
+        devShell = pkgs.mkShell {
+          packages = [ssprove];
+          shellHook = '' alias ll="ls -lasi" '';
+        };
+      }
+    );
+}
diff --git a/.nix/flake.nix.template_versioned b/.nix/flake.nix.template_versioned
new file mode 100644
index 00000000..c1e7135a
--- /dev/null
+++ b/.nix/flake.nix.template_versioned
@@ -0,0 +1,30 @@
+{
+  inputs = {
+    nixpkgs.url        = github:nixos/nixpkgs;
+    flake-utils.url    = github:numtide/flake-utils;
+
+    ## We have start using Nix flakes only after version 0.2.0.
+    ## Hence, loading versions flake-style works best after
+    ## version 0.2.0.
+    # ssprove.url = github:ssprove/ssprove/nix;
+    # ssprove.inputs.nixpkgs.follows = "nixpkgs";
+    # ssprove.inputs.flake-utils.follows = "flake-utils";
+ };
+  outputs = { self, nixpkgs, flake-utils
+            #, ssprove
+            }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let
+        pkgs = nixpkgs.legacyPackages.${system};
+        coqPackages = pkgs.coqPackages_8_17.overrideScope
+          (self: super:{
+            ssprove = super.ssprove.override { version = "0.1.0"; };
+          });
+      in {
+        devShell = pkgs.mkShell {
+          packages = (with coqPackages; [ssprove]);
+          shellHook = '' alias ll="ls -lasi" '';
+        };
+      }
+    );
+}
diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix
new file mode 100644
index 00000000..551bfce5
--- /dev/null
+++ b/.nix/nixpkgs.nix
@@ -0,0 +1,4 @@
+fetchTarball {
+         url = https://github.com/NixOS/nixpkgs/archive/045a097bde2100af7301e50632a02d0425031042.tar.gz;
+         sha256 = "1gw6xkyzhc08q93dkb6p2s0c8b7vhj9nq5amwn5146ag38cp0j3l";
+       }
diff --git a/DOC.md b/DOC.md
index 30829a04..c3000d04 100644
--- a/DOC.md
+++ b/DOC.md
@@ -437,6 +437,9 @@ but where the set of locations is internalised.
 `package` then, `{package p₀ ∘ p₁ }` is a valid expression, and will be complete
 if the interfaces match.
 
+**Note:** When using `Equations`, please `Set Equations Transparent` such
+that code simplification in proofs via `ssprove_code_simpl` resolves properly.
+
 ## High-level SSP proofs
 
 To reason at the high-level of state-separating proofs, we have two main
@@ -1196,4 +1199,4 @@ develop something more general. 🚧
 
 [extructures]: https://github.com/arthuraa/extructures
 
-[open an issue]: https://github.com/SSProve/ssprove/issues
\ No newline at end of file
+[open an issue]: https://github.com/SSProve/ssprove/issues
diff --git a/README.md b/README.md
index 6e4374b9..9e9261ba 100644
--- a/README.md
+++ b/README.md
@@ -33,17 +33,25 @@ A documentation is available in [DOC.md].
 
 ## Installation
 
+There are two installation options:
+- via `opam`
+- via `nix`
+
 #### Prerequisites
 
-- OCaml `>=4.05.0 & <5`
-- Coq `>=8.16.0 & <8.18.0`
-- Equations `1.3`
-- Mathcomp `>=1.15.0`
-- Mathcomp analysis `>=0.5.3`
-- Coq Extructures `0.3.1`
-- Coq Deriving `0.1`
+- OCaml
+- Coq
+- Equations
+- Mathcomp
+- Mathcomp analysis
+- Coq Extructures
+- Coq Deriving
+
+
+### OPAM-based installation
 
-You can get them all from the `opam` package manager for OCaml:
+
+You can get all dependencies from the `opam` package manager for OCaml:
 ```sh
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam update
@@ -53,6 +61,35 @@ opam install ./ssprove.opam
 To build the dependency graph, you can optionally install `graphviz`.
 On macOS, `gsed` is additionally required for this.
 
+### Nix-based installation
+
+`ssprove` is available on `nixpkgs`, e.g., `coqPackages_8_19.ssprove`.
+The following flake-based templates for your new SSProve project are available:
+- [SSProve latest](.nix/flake.nix.template_latest) -- provides a project setup
+with the latest SSProve development readily installed.
+- [SSProve versioned](.nix/flake.nix.template_versioned) -- provides
+a Nix flake that loads a dedicated version (that you may change).
+
+#### Quick start guide
+
+##### Nix installation
+This is performed only once.
+1. [Install Nix](https://nix.dev/install-nix.html) with `curl -L https://nixos.org/nix/install | sh -s -- --daemon`
+2. Enable [flake support](https://nixos.wiki/wiki/Flakes) with `mkdir -p ~/.config/nix && echo -e "experimental-features = nix-command flakes" >> ~/.config/nix/nix.conf`
+All set.
+
+##### Project setup
+1. Create a new project folder and `cd` into it.
+2. Copy one of the above templates into it (removing the `.template*` suffix).
+3. And finally run `nix develop` which throws you into a shell where SSProve is already installed. (`From Crypt Require Import ...`)
+
+You may need to initialize the project as a Git repository and add the `flake.nix` to it.
+The generated `flake.lock` pins the versions and hence also needs to be added to this new project repo.
+
+In the `flake.nix`, you can add [more Coq packages from the Nix repository](https://github.com/NixOS/nixpkgs/blob/a194f9d0654e368fb900830a19396f9d7792647a/pkgs/top-level/coq-packages.nix#L20).
+
+## Build instructions
+
 #### Running verification
 
 Run `make` from this directory to verify all the Coq files.
@@ -63,12 +100,12 @@ Run `make graph` to build a graph of dependencies between sources.
 
 ## Directory organisation
 
-| Directory             | Description                                          |
-|-----------------------|------------------------------------------------------|
-| [theories]           | Root of all the Coq files                            |
-| [theories/Mon]        | External development coming from "Dijkstra Monads For All" |
-| [theories/Relational] | External development coming from "The Next 700 Relational Program Logics"|
-| [theories/Crypt]      | This paper                                           |
+| Directory             | Description                                                               |
+|-----------------------|---------------------------------------------------------------------------|
+| [theories]            | Root of all the Coq files                                                 |
+| [theories/Mon]        | External development coming from "Dijkstra Monads For All"                |
+| [theories/Relational] | External development coming from "The Next 700 Relational Program Logics" |
+| [theories/Crypt]      | This paper                                                                |
 
 Unless specified with a full path, all files considered in this README can
 safely be assumed to be in [theories/Crypt].
diff --git a/default.nix b/default.nix
new file mode 100644
index 00000000..1a24d7a1
--- /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)
diff --git a/flake.lock b/flake.lock
index 49c856c9..0f791735 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1705309234,
-        "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=",
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
         "type": "github"
       },
       "original": {
@@ -20,11 +20,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1707824078,
-        "narHash": "sha256-Au3wLi2d06bU7TDvahP2jIEeKwmjAxKHqi8l2uiBkGA=",
+        "lastModified": 1717096212,
+        "narHash": "sha256-1Tti/eg2jTKYiVonCCjy+DnJspZ5q+tw9+C/bV9y0mg=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "99d7b32e4cfdaf763d9335b4d9ecf4415cbdc405",
+        "rev": "afd3a57b83977a2e0fe8c4685ca2016a12103d03",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index cf4bfc64..3098a73e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,48 +5,45 @@
   };
   outputs = { self, nixpkgs, flake-utils }:
     let
-      mkDrv = { stdenv, which, coqPackages, coq } :
-           let
-             extructures' = coqPackages.extructures.override { version = "0.4.0"; };
-           in
-            stdenv.mkDerivation {
-              pname = "ssprove";
-              version = "0.0.1";
-              src = ./.;
-              nativeBuildInputs = [ which coq.ocamlPackages.findlib ] ++
-                                  (with coqPackages; [
-                                    equations
-                                    mathcomp-analysis
-                                    mathcomp-ssreflect
-                                    deriving
-                                  ])
-                                  ++ [extructures'];
-              buildInputs = [ coq ];
-            };
-    in { inherit mkDrv; } //
-      flake-utils.lib.eachDefaultSystem (system:
-        let
-          pkgs = nixpkgs.legacyPackages.${system};
-        in
-         rec {
-            devShell =
-              let
-                args = {
-                  inherit (pkgs) stdenv which;
-                  coq = pkgs.coq_8_18;
-                  coqPackages = pkgs.coqPackages_8_18.overrideScope
-                    (self: super: {
-                      mathcomp = super.mathcomp.override { version = "2.1.0"; };
-                      mathcomp-analysis = super.mathcomp-analysis.override { version = "1.0.0"; };
-                    });
-                };
-                ssprove' = mkDrv args;
-              in
-                pkgs.mkShell {
-                  packages =
-                    (with pkgs; [ coq gnumake ])
-                    ++
-                    (with ssprove';  nativeBuildInputs);
-                };
-         });
+      ssprovePkg = { lib, mkCoqDerivation, coq
+                  , equations, extructures, deriving
+                  , mathcomp-analysis, mathcomp-ssreflect }:
+        mkCoqDerivation {
+          pname = "ssprove";
+          owner = "SSProve";
+          version = "0.2.0";
+          src = ./.;
+          propagatedBuildInputs = [
+            equations
+            mathcomp-analysis
+            mathcomp-ssreflect
+            deriving
+            extructures
+          ];
+          meta = {
+            description = "A foundational framework for modular cryptographic proofs in Coq ";
+            license = lib.licenses.mit;
+          };
+        };
+    in {
+      overlays.default = final: prev: {
+        coqPackages_8_19 = prev.coqPackages_8_19.overrideScope (self: super: {
+          # mathcomp-ssreflect inherits this version
+          # setting it to mathcomp-ssreflect does not work.
+          # see my question on Zulip:
+          # https://coq.zulipchat.com/#narrow/stream/290990-Nix-toolbox-devs-.26-users/topic/Loading.20inconsistency.20in.20mathcomp.20dependencies
+          mathcomp = super.mathcomp.override { version = "2.2.0"; };
+          ssprove  = self.callPackage ssprovePkg {};
+        });
+      };
+    } // flake-utils.lib.eachDefaultSystem (system:
+      let
+        pkgs = import nixpkgs {
+          inherit system;
+          overlays = [ self.overlays.default ];
+        };
+      in {
+        packages.default = pkgs.coqPackages_8_19.ssprove;
+        devShells.default = self.packages.${system}.default;
+      });
 }