diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml
index 565bdf6ec..6f2411ba2 100644
--- a/.github/workflows/nix-action-coq-8.19.yml
+++ b/.github/workflows/nix-action-coq-8.19.yml
@@ -1,6 +1,7 @@
 jobs:
-  coq:
-    needs: []
+  QuickChick:
+    needs:
+    - mathcomp-ssreflect
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -37,18 +38,223 @@ jobs:
         extraPullNames: coq, coq-community, math-comp
         name: coq-elpi
     - id: stepCheck
-      name: Checking presence of CI target coq
+      name: Checking presence of CI target QuickChick
       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 \"QuickChick\" \\\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: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "mathcomp-ssreflect"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq-ext-lib'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "coq-ext-lib"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: simple-io'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "simple-io"
+    - 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 "QuickChick"
+  Verdi:
+    needs:
+    - mathcomp-ssreflect
+    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-elpi
+      uses: cachix/cachix-action@v12
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target Verdi
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.19\" --argstr job \"Verdi\" \\\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 "coq-8.19"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: Cheerios'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "Cheerios"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: InfSeqExt'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "InfSeqExt"
+    - 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 "coq-8.19"
+        --argstr job "mathcomp-ssreflect"
+    - 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 "Verdi"
+  addition-chains:
+    needs:
+    - mathcomp-ssreflect
+    - mathcomp-algebra
+    - mathcomp-fingroup
+    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-elpi
+      uses: cachix/cachix-action@v12
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target addition-chains
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.19\" --argstr job \"addition-chains\" \\\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: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "mathcomp-ssreflect"
+    - 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 "coq-8.19"
+        --argstr job "mathcomp-algebra"
+    - 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 "coq-8.19"
+        --argstr job "mathcomp-fingroup"
+    - 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 "coq-8.19"
+        --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 "coq-8.19"
+        --argstr job "addition-chains"
+  autosubst:
+    needs:
+    - mathcomp-ssreflect
+    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-elpi
+      uses: cachix/cachix-action@v12
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target autosubst
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.19\" --argstr job \"autosubst\" \\\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 "coq-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 "coq-8.19"
+        --argstr job "mathcomp-ssreflect"
+    - 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 "autosubst"
   coq-elpi:
-    needs:
-    - coq
+    needs: []
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -98,9 +304,120 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
         --argstr job "coq-elpi"
+  coquelicot:
+    needs:
+    - mathcomp-ssreflect
+    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-elpi
+      uses: cachix/cachix-action@v12
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target coquelicot
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.19\" --argstr job \"coquelicot\" \\\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: mathcomp-ssreflect'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "mathcomp-ssreflect"
+    - 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 "coquelicot"
+  deriving:
+    needs:
+    - mathcomp-ssreflect
+    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-elpi
+      uses: cachix/cachix-action@v12
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target deriving
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.19\" --argstr job \"deriving\" \\\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 "coq-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 "coq-8.19"
+        --argstr job "mathcomp-ssreflect"
+    - 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 "deriving"
   hierarchy-builder:
     needs:
-    - coq
     - coq-elpi
     runs-on: ubuntu-latest
     steps:
@@ -155,9 +472,82 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
         --argstr job "hierarchy-builder"
+  interval:
+    needs:
+    - coquelicot
+    - mathcomp-ssreflect
+    - mathcomp-fingroup
+    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-elpi
+      uses: cachix/cachix-action@v12
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target interval
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.19\" --argstr job \"interval\" \\\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 "coq-8.19"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: bignums'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "bignums"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coquelicot'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "coquelicot"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: flocq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
+        --argstr job "flocq"
+    - 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 "coq-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 "coq-8.19"
+        --argstr job "mathcomp-fingroup"
+    - 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 "interval"
   mathcomp:
     needs:
-    - coq
     - mathcomp-ssreflect
     - mathcomp-fingroup
     - mathcomp-algebra
@@ -244,7 +634,6 @@ jobs:
         --argstr job "mathcomp"
   mathcomp-algebra:
     needs:
-    - coq
     - mathcomp-ssreflect
     - mathcomp-fingroup
     - hierarchy-builder
@@ -311,7 +700,6 @@ jobs:
         --argstr job "mathcomp-algebra"
   mathcomp-analysis:
     needs:
-    - coq
     - mathcomp-classical
     - mathcomp-field
     - mathcomp-bigenough
@@ -383,7 +771,6 @@ jobs:
         --argstr job "mathcomp-analysis"
   mathcomp-bigenough:
     needs:
-    - coq
     - mathcomp-ssreflect
     runs-on: ubuntu-latest
     steps:
@@ -440,7 +827,6 @@ jobs:
         --argstr job "mathcomp-bigenough"
   mathcomp-character:
     needs:
-    - coq
     - mathcomp-ssreflect
     - mathcomp-fingroup
     - mathcomp-algebra
@@ -522,7 +908,6 @@ jobs:
         --argstr job "mathcomp-character"
   mathcomp-classical:
     needs:
-    - coq
     - mathcomp-algebra
     - mathcomp-finmap
     - hierarchy-builder
@@ -589,7 +974,6 @@ jobs:
         --argstr job "mathcomp-classical"
   mathcomp-field:
     needs:
-    - coq
     - mathcomp-ssreflect
     - mathcomp-fingroup
     - mathcomp-algebra
@@ -666,7 +1050,6 @@ jobs:
         --argstr job "mathcomp-field"
   mathcomp-fingroup:
     needs:
-    - coq
     - mathcomp-ssreflect
     - hierarchy-builder
     runs-on: ubuntu-latest
@@ -728,7 +1111,6 @@ jobs:
         --argstr job "mathcomp-fingroup"
   mathcomp-finmap:
     needs:
-    - coq
     - mathcomp-ssreflect
     runs-on: ubuntu-latest
     steps:
@@ -785,7 +1167,6 @@ jobs:
         --argstr job "mathcomp-finmap"
   mathcomp-solvable:
     needs:
-    - coq
     - mathcomp-ssreflect
     - mathcomp-fingroup
     - mathcomp-algebra
@@ -857,7 +1238,6 @@ jobs:
         --argstr job "mathcomp-solvable"
   mathcomp-ssreflect:
     needs:
-    - coq
     - hierarchy-builder
     runs-on: ubuntu-latest
     steps:
@@ -914,7 +1294,6 @@ jobs:
         --argstr job "mathcomp-ssreflect"
   odd-order:
     needs:
-    - coq
     - mathcomp-character
     - mathcomp-ssreflect
     - mathcomp-fingroup
@@ -999,6 +1378,62 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19"
         --argstr job "odd-order"
+  reglang:
+    needs:
+    - mathcomp-ssreflect
+    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-elpi
+      uses: cachix/cachix-action@v12
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, coq-community, math-comp
+        name: coq-elpi
+    - id: stepCheck
+      name: Checking presence of CI target reglang
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-8.19\" --argstr job \"reglang\" \\\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 "coq-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 "coq-8.19"
+        --argstr job "mathcomp-ssreflect"
+    - 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 "reglang"
 name: Nix CI for bundle coq-8.19
 'on':
   pull_request:
diff --git a/.nix/config.nix b/.nix/config.nix
index 4b4203657..3b7b4e899 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -5,7 +5,6 @@
   bundles = {
 
     "coq-8.19".coqPackages = {
-      coq.override.version = "8.19+rc1";
       
       hierarchy-builder.override.version = "master";
       hierarchy-builder-shim.job = false;
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
index 2ca14687e..228cfca2f 100644
--- a/.nix/coq-nix-toolbox.nix
+++ b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"dd771a5001cd955514f2462cad7cdd90377530e3"
+"c78e8070b98eb9f20316d743cb0305759ffbfdf0"
diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix
index 90f8e03ea..fd353be75 100644
--- a/.nix/coq-overlays/coq-elpi/default.nix
+++ b/.nix/coq-overlays/coq-elpi/default.nix
@@ -12,6 +12,8 @@ with builtins; with lib; let
     { case = "8.18"; out = { version = "v1.18.1"; };}
     { case = "8.19"; out = { version = "v1.18.2"; };}
   ] {} );
+  dot-merlin-reader = coq.ocamlPackages.dot-merlin-reader;
+  dune = coq.ocamlPackages.dune_3;
 in mkCoqDerivation {
   pname = "elpi";
   repo  = "coq-elpi";
@@ -64,7 +66,7 @@ in mkCoqDerivation {
   buildFlags = [ "OCAMLWARN=" ];
 
   mlPlugin = true;
-  propagatedBuildInputs = [ coq.ocamlPackages.findlib elpi ];
+  propagatedBuildInputs = [ coq.ocamlPackages.findlib elpi dot-merlin-reader dune ];
 
   meta = {
     description = "Coq plugin embedding ELPI.";
diff --git a/.nix/ocaml-overlays/elpi/default.nix b/.nix/ocaml-overlays/elpi/default.nix
index 2af439cad..ff8ae0ba3 100644
--- a/.nix/ocaml-overlays/elpi/default.nix
+++ b/.nix/ocaml-overlays/elpi/default.nix
@@ -1,6 +1,7 @@
 { lib
 , buildDunePackage, camlp5
 , ocaml
+, ocaml-lsp
 , menhir, menhirLib
 , atdgen
 , stdlib-shims
@@ -47,10 +48,11 @@ buildDunePackage rec {
   buildInputs = [ ncurses ]
   ++ lib.optional (lib.versionAtLeast version "1.16" || version == "dev") atdgen;
 
-  propagatedBuildInputs = [ re stdlib-shims ]
-  ++ [ menhirLib ]
-  ++ [ ppxlib ppx_deriving ]
-  ;
+  propagatedBuildInputs = [ re stdlib-shims ocaml-lsp ]
+  ++ (if lib.versionAtLeast version "1.15" || version == "dev"
+     then [ menhirLib ]
+     else [ camlp5 ] )
+  ++ [ ppxlib ppx_deriving atdgen ];
 
   meta = with lib; {
     description = "Embeddable λProlog Interpreter";
diff --git a/Changelog.md b/Changelog.md
index fc7f2cef4..08234afcb 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,6 +1,6 @@
 # Changelog
 
-## [2.0.2] - 01/02/2024
+## [2.0.2] - 12/02/2024
 
 Requires Elpi 1.18.2 and Coq 8.19.
 
@@ -8,6 +8,8 @@ Requires Elpi 1.18.2 and Coq 8.19.
 - Fix `coq.elaborate-*` does not erase the type annotation of `Let`s (regression
   introduced in 2.0.1). This fix may introduce differences in generated names
 - Fix `coq.elaborate-*` are not affected anymore by printing options
+- New `coq.univ.alg-super` that relates a univ `U` to its algebraic successor
+  `V`, that is `U+1` and not any `V` s.t. `U < V`
 
 ### Commands
 - Fix install the right initial parsing state (the one before any synterp action
@@ -17,6 +19,8 @@ Requires Elpi 1.18.2 and Coq 8.19.
 - Fix evar instantiation loss when crossing the elpi/ltac border
 - Fix encoding of "definitional classes" (`Class` with no record)
 - Fix order of implicit arguments of `Record`
+- New `@keep-alg-univs!` option for all APIs taking terms. By default algebraic
+  universes are replaced by named universes. See the `coq.univ.alg-super` API.
 
 ### Misc
 - Change requiring `elpi` does not load primitive integers nor primitive floats
diff --git a/_CoqProject b/_CoqProject
index 29a5f0cb1..dc932f8e3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,5 @@
 -arg -w -arg +elpi.deprecated
+-arg -w -arg -ambiguous-extra-dep
 
 -R theories elpi
 -Q examples elpi.examples
diff --git a/apps/NES/_CoqProject b/apps/NES/_CoqProject
index 116cb4bb4..ea722808f 100644
--- a/apps/NES/_CoqProject
+++ b/apps/NES/_CoqProject
@@ -8,3 +8,5 @@
 
 theories/NES.v
 
+-arg -w -arg -ambiguous-extra-dep
+
diff --git a/apps/coercion/_CoqProject b/apps/coercion/_CoqProject
index b5b8d84f0..a9903c162 100644
--- a/apps/coercion/_CoqProject
+++ b/apps/coercion/_CoqProject
@@ -12,3 +12,5 @@ src/elpi_coercion_plugin.mlpack
 src/META.coq-elpi-coercion
 
 theories/coercion.v
+
+-arg -w -arg -ambiguous-extra-dep
diff --git a/apps/cs/_CoqProject b/apps/cs/_CoqProject
index 39ac91fab..937f00fbe 100644
--- a/apps/cs/_CoqProject
+++ b/apps/cs/_CoqProject
@@ -13,3 +13,5 @@ src/elpi_cs_plugin.mlpack
 src/META.coq-elpi-cs
 
 theories/cs.v
+
+-arg -w -arg -ambiguous-extra-dep
diff --git a/apps/derive/_CoqProject b/apps/derive/_CoqProject
index de3a997ba..997fc9f4a 100644
--- a/apps/derive/_CoqProject
+++ b/apps/derive/_CoqProject
@@ -39,3 +39,5 @@ theories/derive/eqb.v
 theories/derive/eqbcorrect.v
 theories/derive/eqbOK.v
 theories/derive/eqType_ast.v
+
+-arg -w -arg -ambiguous-extra-dep
diff --git a/apps/eltac/_CoqProject b/apps/eltac/_CoqProject
index 85f861b7a..8ff2e8fbd 100644
--- a/apps/eltac/_CoqProject
+++ b/apps/eltac/_CoqProject
@@ -20,3 +20,5 @@ theories/case.v
 theories/generalize.v
 theories/cycle.v
 theories/tactics.v
+
+-arg -w -arg -ambiguous-extra-dep
diff --git a/apps/locker/_CoqProject b/apps/locker/_CoqProject
index 2adcf48f6..ce4e1f649 100644
--- a/apps/locker/_CoqProject
+++ b/apps/locker/_CoqProject
@@ -7,3 +7,5 @@
 -Q elpi elpi.apps.locker
 
 theories/locker.v
+
+-arg -w -arg -ambiguous-extra-dep
diff --git a/apps/tc/_CoqProject b/apps/tc/_CoqProject
index 7898332a8..6244fdc12 100644
--- a/apps/tc/_CoqProject
+++ b/apps/tc/_CoqProject
@@ -20,3 +20,5 @@ theories/db.v
 theories/add_commands.v
 theories/tc.v
 theories/wip.v
+
+-arg -w -arg -ambiguous-extra-dep
\ No newline at end of file
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index d5a2085af..ab535ec03 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -452,6 +452,8 @@ typeabbrev opaque?   bool.  macro @opaque! :- tt. macro @transparent! :- ff.
 
 %%%%%%% Attributes to be passed to APIs as in @local! => coq.something %%%%%%%%
 
+macro @keep-alg-univs! :- get-option "coq:keepalgunivs" tt.
+
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @reversible! :- get-option "coq:reversible" tt. % coercions
 macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference 
@@ -952,8 +954,7 @@ typeabbrev univ (ctype "univ").
 kind sort type.
 type prop sort. % impredicative sort of propositions
 type sprop sort. % impredicative sort of propositions with definitional proof irrelevance
-type typ univ ->
-         sort. % predicative sort of data (carries a universe level)
+type typ univ -> sort. % predicative sort of data (carries a universe level)
 
 % [coq.sort.leq S1 S2] constrains S1 <= S2
 external pred coq.sort.leq o:sort, o:sort.
@@ -974,6 +975,10 @@ external pred coq.univ.print .
 % [coq.univ.new U] A fresh universe.
 external pred coq.univ.new o:univ.
 
+% [coq.univ.alg-super U V] relates a univ U to its algebraic successor V,
+% that is U+1 and not any V s.t. U < V
+external pred coq.univ.alg-super i:univ, o:univ.
+
 % [coq.univ Name U] Finds a named unvierse. Can fail.
 external pred coq.univ o:id, o:univ.
 
diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi
index bd7d8ebb0..ba475302d 100644
--- a/elpi/coq-HOAS.elpi
+++ b/elpi/coq-HOAS.elpi
@@ -301,6 +301,8 @@ typeabbrev opaque?   bool.  macro @opaque! :- tt. macro @transparent! :- ff.
 
 %%%%%%% Attributes to be passed to APIs as in @local! => coq.something %%%%%%%%
 
+macro @keep-alg-univs! :- get-option "coq:keepalgunivs" tt.
+
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @reversible! :- get-option "coq:reversible" tt. % coercions
 macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference 
diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 4c771cccc..227af9112 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -166,45 +166,6 @@ let isuniv, univout, (univ : Univ.Universe.t API.Conversion.t) =
     | _ -> univ_to_be_patched.API.Conversion.readback ~depth state t
   end
 }
-
-let sort =
-  let open API.AlgebraicData in  declare {
-  ty = API.Conversion.TyName "sort";
-  doc = "Sorts (kinds of types)";
-  pp = (fun fmt -> function
-    | Sorts.Type _ -> Format.fprintf fmt "Type"
-    | Sorts.Set -> Format.fprintf fmt "Set"
-    | Sorts.Prop -> Format.fprintf fmt "Prop"
-    | Sorts.SProp -> Format.fprintf fmt "SProp"
-    | Sorts.QSort _ -> Format.fprintf fmt "Type");
-  constructors = [
-    K("prop","impredicative sort of propositions",N,
-      B Sorts.prop,
-      M (fun ~ok ~ko -> function Sorts.Prop -> ok | _ -> ko ()));
-    K("sprop","impredicative sort of propositions with definitional proof irrelevance",N,
-      B Sorts.sprop,
-      M (fun ~ok ~ko -> function Sorts.SProp -> ok | _ -> ko ()));
-    K("typ","predicative sort of data (carries a universe level)",A(univ,N),
-      B (fun x -> Sorts.sort_of_univ x),
-      M (fun ~ok ~ko -> function
-        | Sorts.Type x -> ok x
-        | Sorts.Set -> ok Univ.Universe.type0
-        | _ -> ko ()));
-    K("uvar","",A(F.uvar,N),
-      BS (fun (k,_) state ->
-        let m = S.get um state in
-        try
-          let u = UM.host k m in
-          state, Sorts.sort_of_univ u
-        with Not_found ->
-          let state, (_,u) = new_univ_level_variable state in
-          let state = S.update um state (UM.add k u) in
-          state, Sorts.sort_of_univ u),
-      M (fun ~ok ~ko _ -> ko ()));
-  ]
-} |> API.ContextualConversion.(!<)
-
-
 let universe_level_variable =
   let { CD.cin = levelin }, universe_level_variable_to_patch = CD.declare {
     CD.name = "univ.variable";
@@ -347,6 +308,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  algunivs : bool option;
 }
 
 let default_options () = {
@@ -366,6 +328,7 @@ let default_options () = {
   keepunivs = None;
   redflags = None;
   no_tc = None;
+  algunivs = None;
 }
 
 type 'a coq_context = {
@@ -398,6 +361,59 @@ let pr_coq_ctx { env; db2name; db2rel } sigma =
     v 0 (Printer.pr_rel_context_of env sigma) ++ cut ()
   )
 
+let propc   = E.Constants.declare_global_symbol "prop"
+let spropc   = E.Constants.declare_global_symbol "sprop"
+let typc   = E.Constants.declare_global_symbol "typ"
+
+
+let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversion.t =
+  let open API.ContextualConversion in
+  {
+  ty = API.Conversion.TyName "sort";
+  pp_doc = (fun fmt () ->
+    Format.fprintf fmt "%% Sorts (kinds of types)\n";
+    Format.fprintf fmt "kind sort type.\n";
+    Format.fprintf fmt "type prop sort. %% impredicative sort of propositions\n";
+    Format.fprintf fmt "type sprop sort. %% impredicative sort of propositions with definitional proof irrelevance\n";
+    Format.fprintf fmt "type typ univ -> sort. %% predicative sort of data (carries a universe level)\n";
+  );
+  pp = (fun fmt -> function
+    | Sorts.Type _ -> Format.fprintf fmt "Type"
+    | Sorts.Set -> Format.fprintf fmt "Set"
+    | Sorts.Prop -> Format.fprintf fmt "Prop"
+    | Sorts.SProp -> Format.fprintf fmt "SProp"
+    | Sorts.QSort _ -> Format.fprintf fmt "QSort");
+  embed = (fun ~depth { options } _ state s ->
+    match s with
+    | Sorts.Prop -> state, E.mkConst propc, []
+    | Sorts.SProp -> state, E.mkConst spropc, []
+    | Sorts.Set ->
+        let state, u, gls = univ.embed ~depth state Univ.Universe.type0 in
+        state, E.mkApp typc u [], gls
+    | Sorts.Type u ->
+        let state, u, gls = univ.embed ~depth state u in
+        state, E.mkApp typc u [], gls
+    | Sorts.QSort _ -> nYI "sort polymorphism");
+  readback = (fun ~depth { options } _ state t ->
+    match E.look ~depth t with
+    | E.Const c when c == propc -> state, Sorts.prop, []
+    | E.Const c when c == spropc -> state, Sorts.sprop, []
+    | E.App(c,u,[]) when c == typc ->
+        let state, u, gls = univ.readback ~depth state u in
+        state, Sorts.sort_of_univ u ,gls
+    | E.UnifVar(k,_) -> begin
+        let m = S.get um state in
+        try
+          let u = UM.host k m in
+          state, Sorts.sort_of_univ u, []
+        with Not_found ->
+          let state, (_,u) = new_univ_level_variable state in
+          let state = S.update um state (UM.add k u) in
+          state, Sorts.sort_of_univ u, []
+        end
+    | _ ->  raise API.Conversion.(TypeErr(TyName"sort",depth,t)));
+}
+
 let in_coq_fresh ~id_only =
   let mk_fresh dbl =
     Id.of_string_soft
@@ -947,17 +963,20 @@ let purge_algebraic_univs_sort state s =
       let state, _, _, s = force_level_of_universe state u in
       state, s
   | x -> state, x
-
+  
+let sort = { sort with API.ContextualConversion.embed = (fun ~depth ctx csts state s ->
+  let state, s =
+    if ctx.options.algunivs = None || ctx.options.algunivs = Some false then
+      purge_algebraic_univs_sort state (EConstr.ESorts.make s)
+    else
+      state, s in
+  sort.API.ContextualConversion.embed ~depth ctx csts state s) }
+  
 let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []
-
-let sort = { sort with API.Conversion.embed = (fun ~depth state s ->
-  let state, s = purge_algebraic_univs_sort state (EConstr.ESorts.make s) in
-  sort.API.Conversion.embed ~depth state s) }
-
-let in_elpi_sort ~depth state s =
-  let state, s, gl = sort.API.Conversion.embed ~depth state s in
-  assert(gl=[]);
-  state, E.mkApp sortc s []
+  
+let in_elpi_sort ~depth ctx csts state s =
+  let state, s, gl = sort.API.ContextualConversion.embed ~depth ctx csts state s in
+  state, E.mkApp sortc s [], gl
 
 
 (* ********************************* }}} ********************************** *)
@@ -1168,9 +1187,8 @@ let get_options ~depth hyps state =
     no_tc = get_bool_option "coq:no_tc";
     keepunivs = get_bool_option "coq:keepunivs";
     redflags = get_redflags_option ();
-
+    algunivs = get_bool_option "coq:keepalgunivs";
   }
-
 let mk_coq_context ~options state =
   let env = get_global_env state in
   let section = section_ids env in
@@ -1312,7 +1330,10 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
          let args = CList.firstn argno args in
          let state, args = CList.fold_left_map (aux ~depth env) state args in
          state, E.mkUnifVar elpi_uvk ~args:(List.rev args) state
-    | C.Sort s -> in_elpi_sort ~depth state (EC.ESorts.kind sigma s)
+    | C.Sort s ->
+         let state, s, gl = in_elpi_sort ~depth coq_ctx API.RawData.no_constraints state (EC.ESorts.kind sigma s) in
+         gls := gl @ !gls;
+         state, s
     | C.Cast (t,_,ty0) ->
          let state, t = aux ~depth env state t in
          let state, ty = aux ~depth env state ty0 in
@@ -1823,7 +1844,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
   debug Pp.(fun () -> str"lp2term@" ++ int depth ++ str":" ++ str(pp2string (P.term depth) t));
   match E.look ~depth t with
   | E.App(s,p,[]) when sortc == s ->
-      let state, u, gsl = sort.API.Conversion.readback ~depth state p in
+      let state, u, gsl = sort.API.ContextualConversion.readback ~depth coq_ctx syntactic_constraints state p in
       state, EC.mkSort (EC.ESorts.make u), gsl
  (* constants *)
   | E.App(c,d,[]) when globalc == c ->
diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli
index b96405847..dab2a79d6 100644
--- a/src/coq_elpi_HOAS.mli
+++ b/src/coq_elpi_HOAS.mli
@@ -47,6 +47,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  algunivs : bool option;
 }
 
 type 'a coq_context = {
@@ -147,7 +148,7 @@ val in_elpi_gr : depth:int -> State.t -> Names.GlobRef.t -> term
 val in_elpi_poly_gr : depth:int -> State.t -> Names.GlobRef.t -> term -> term
 val in_elpi_poly_gr_instance : depth:int -> State.t -> Names.GlobRef.t -> UVars.Instance.t -> term
 val in_elpi_flex_sort : term -> term
-val in_elpi_sort : depth:int -> state -> Sorts.t -> state * term
+val in_elpi_sort : depth:int -> 'a coq_context -> constraints -> state -> Sorts.t -> state * term * Conversion.extra_goals
 val in_elpi_prod : Name.t -> term -> term -> term
 val in_elpi_lam : Name.t -> term -> term -> term
 val in_elpi_let : Name.t -> term -> term -> term -> term
@@ -172,7 +173,7 @@ val gref : Names.GlobRef.t Conversion.t
 val inductive : inductive Conversion.t
 val constructor : constructor Conversion.t
 val constant : global_constant Conversion.t
-val sort : Sorts.t Conversion.t
+val sort : (Sorts.t,'a coq_context,constraints) ContextualConversion.t
 val global_constant_of_globref : Names.GlobRef.t -> global_constant
 val abbreviation : Globnames.abbreviation Conversion.t
 val implicit_kind : Glob_term.binding_kind Conversion.t
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 042f1d276..d7cb6ce1a 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -15,7 +15,7 @@ module B = struct
   let ioarg_any = API.BuiltInPredicate.ioarg_any
   let ioargC = API.BuiltInPredicate.ioargC
   let ioargC_flex = API.BuiltInPredicate.ioargC_flex
-  let ioarg_flex = API.BuiltInPredicate.ioarg_flex
+  (*let ioarg_flex = API.BuiltInPredicate.ioarg_flex*)
   let ioarg_poly s = { ioarg_any with API.Conversion.ty = API.Conversion.TyName s }
 end
 module Pred = API.BuiltInPredicate
@@ -367,7 +367,7 @@ let cs_pattern =
     K("cs-default","",N,
       B Default_cs,
       M (fun ~ok ~ko -> function Default_cs -> ok | _ -> ko ()));
-    K("cs-sort","",A(sort,N),
+    K("cs-sort","",CA(sort,N),
       B (fun s -> Sort_cs (Sorts.family s)),
       MS (fun ~ok ~ko p state -> match p with
         | Sort_cs Sorts.InSet -> ok Sorts.set state
@@ -378,18 +378,18 @@ let cs_pattern =
               ok u state
         | _ -> ko state))
   ]
-} |> CConv.(!<)
+} 
 
 let cs_instance = let open Conv in let open API.AlgebraicData in let open Structures.CSTable in declare {
   ty = TyName "cs-instance";
   doc = "Canonical Structure instances: (cs-instance Proj ValPat Inst)";
   pp = (fun fmt { solution } -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((Printer.pr_global solution)));
   constructors = [
-    K("cs-instance","",A(gref,A(cs_pattern,A(gref,N))),
+    K("cs-instance","",A(gref,CA(cs_pattern,A(gref,N))),
       B (fun p v i -> assert false),
       M (fun ~ok ~ko { solution; value; projection } -> ok projection value solution))
   ]
-} |> CConv.(!<)
+}
 
 
 type tc_priority = Computed of int | UserGiven of int
@@ -2275,40 +2275,46 @@ The different data types stay, since Coq will eventually become
 able to handle algebraic universes consistently, making this purging
 phase unnecessary.|};
   MLData univ;
-  MLData sort;
+  MLDataC sort;
 
   MLCode(Pred("coq.sort.leq",
-    InOut(B.ioarg_flex sort, "S1",
-    InOut(B.ioarg_flex sort, "S2",
-    Full(unit_ctx, "constrains S1 <= S2"))),
-  (fun u1 u2 ~depth _ _ state ->
+    CInOut(B.ioargC_flex sort, "S1",
+    CInOut(B.ioargC_flex sort, "S2",
+    Full(global, "constrains S1 <= S2"))),
+  (fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.leq"
+  (fun state ->
     match u1, u2 with
     | Data u1, Data u2 ->
         if Sorts.equal u1 u2 then state, !: u1 +! u2,[]
         else
-          let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in
-          add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[]
-    | _ -> err Pp.(str"coq.sort.leq: called with _ as argument"))),
+          let state, u2 = if true (* options.algunivs != Some true *)
+          then purge_algebraic_univs_sort state (EConstr.ESorts.make u2)
+          else state, u2 in
+        add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[]
+    | _ -> err Pp.(str"coq.sort.leq: called with _ as argument")))),
   DocAbove);
 
   MLCode(Pred("coq.sort.eq",
-    InOut(B.ioarg_flex sort, "S1",
-    InOut(B.ioarg_flex sort, "S2",
-    Full(unit_ctx, "constrains S1 = S2"))),
-  (fun u1 u2 ~depth _ _ state ->
+    CInOut(B.ioargC_flex sort, "S1",
+    CInOut(B.ioargC_flex sort, "S2",
+    Full(global, "constrains S1 = S2"))),
+  (fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.eq"
+  (fun state ->
     match u1, u2 with
     | Data u1, Data u2 ->
       if Sorts.equal u1 u2 then state, !: u1 +! u2,[]
       else
-        let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in
+        let state, u2 = if true (* options.algunivs != Some true *)
+        then purge_algebraic_univs_sort state (EConstr.ESorts.make u2)
+        else state, u2 in
         add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, []
-    | _ -> err Pp.(str"coq.sort.eq: called with _ as argument"))),
+    | _ -> err Pp.(str"coq.sort.eq: called with _ as argument")))),
   DocAbove);
 
   MLCode(Pred("coq.sort.sup",
-    InOut(B.ioarg_flex sort, "S1",
-    InOut(B.ioarg_flex sort, "S2",
-    Full(unit_ctx,  "constrains S2 = S1 + 1"))),
+    CInOut(B.ioargC_flex sort, "S1",
+    CInOut(B.ioargC_flex sort, "S2",
+    Full(global,  "constrains S2 = S1 + 1"))),
   (fun u1 u2 ~depth _ _ state ->
     match u1, u2 with
     | Data u1, Data u2 -> univ_super state u1 u2, !: u1 +! u2, []
@@ -2316,10 +2322,10 @@ phase unnecessary.|};
   DocAbove);
 
   MLCode(Pred("coq.sort.pts-triple",
-    InOut(B.ioarg_flex sort, "S1",
-    InOut(B.ioarg_flex sort, "S2",
-    Out(sort, "S3",
-    Full(unit_ctx,  "constrains S3 = sort of product with domain in S1 and codomain in S2")))),
+    CInOut(B.ioargC_flex sort, "S1",
+    CInOut(B.ioargC_flex sort, "S2",
+    COut(sort, "S3",
+    Full(global,  "constrains S3 = sort of product with domain in S1 and codomain in S2")))),
   (fun u1 u2 _ ~depth _ _ state ->
     match u1, u2 with
     | Data u1, Data u2 -> let state, u3 = univ_product state u1 u2 in state, !: u1 +! u2 +! u3, []
@@ -2344,6 +2350,14 @@ phase unnecessary.|};
      state, !: u, [])),
   DocAbove);
 
+  MLCode(Pred("coq.univ.alg-super",
+    In(univ,"U",
+    Out(univ,"V",
+    Full(unit_ctx,  "relates a univ U to its algebraic successor V, that is U+1 and not any V s.t. U < V"))),
+  (fun u _ ~depth _ _ state ->
+    state, !: (Univ.Universe.super u), [])),
+  DocAbove);
+
   MLCode(Pred("coq.univ",
     InOut(B.ioarg id, "Name",
     InOut(B.ioarg univ, "U",
@@ -2559,8 +2573,8 @@ declared as cumulative.|};
 
   LPDoc "-- Databases (TC, CS, Coercions) ------------------------------------";
 
-  MLData cs_pattern;
-  MLData cs_instance;
+  MLDataC cs_pattern;
+  MLDataC cs_instance;
 
   MLCode(Pred("coq.CS.declare-instance",
     In(gref, "GR",
@@ -2573,7 +2587,7 @@ Supported attributes:
   DocAbove);
 
   MLCode(Pred("coq.CS.db",
-    Out(list cs_instance, "Db",
+    COut(CConv.(!>>) list cs_instance, "Db",
     Read(global,"reads all instances")),
   (fun _ ~depth _ _ _ ->
      !: (Structures.CSTable.(entries ())))),
@@ -2581,8 +2595,8 @@ Supported attributes:
 
   MLCode(Pred("coq.CS.db-for",
     In(B.unspec gref, "Proj",
-    In(B.unspec cs_pattern, "Value",
-    Out(list cs_instance, "Db",
+    CIn(B.unspecC cs_pattern, "Value",
+    COut(CConv.(!>>) list cs_instance, "Db",
     Read(global,"reads all instances for a given Projection or canonical Value, or both")))),
   (fun proj value _ ~depth _ _ state ->
     let env = get_global_env state in
@@ -3176,7 +3190,7 @@ Universe constraints are put in the constraint store.|})))),
 
   MLCode(Pred("coq.typecheck-ty",
     CIn(term,  "Ty",
-    InOut(B.ioarg sort, "U",
+    CInOut(B.ioargC sort, "U",
     InOut(B.ioarg B.diagnostic, "Diagnostic",
     Full (proof_context,
 {|typchecks a type Ty returning its universe U. If U is provided, then
@@ -3297,7 +3311,7 @@ Supported attributes:
 
    MLCode(Pred("coq.elaborate-ty-skeleton",
      CIn(term_skeleton,  "T",
-     Out(sort, "U",
+     COut(sort, "U",
      COut(term,  "E",
      InOut(B.ioarg B.diagnostic, "Diagnostic",
      Full (proof_context,{|elabotares T expecting it to be a type of sort U.
diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
index 62bc3c0e1..118094886 100644
--- a/src/coq_elpi_glob_quotation.ml
+++ b/src/coq_elpi_glob_quotation.ml
@@ -175,8 +175,11 @@ let rec gterm2lp ~depth state x =
       let s = API.RawData.mkUnifVar f ~args:[] state in
       state, in_elpi_flex_sort s
   | GSort(UNamed (None, u)) ->
+      let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state, []) (get_ctx state) in
       let env = get_glob_env state in
-      in_elpi_sort ~depth state (sort_name env (get_sigma state) u)
+      let state, s, gls = in_elpi_sort ~depth ctx E.no_constraints state (sort_name env (get_sigma state) u) in
+      assert(gls = []);
+      state,s
   | GSort(_) -> nYI "(glob)HOAS for Type@{i j}"
 
   | GProd(name,_,s,t) ->
diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v
index cb5d73fba..74ff982ff 100644
--- a/tests/test_API_elaborate.v
+++ b/tests/test_API_elaborate.v
@@ -131,7 +131,6 @@ wrong constant:,
 
 *)
 
-
 Elpi test.API2 Record ind2 (A : T1) := {
    fld1 : A;
    fld2 : fld1 = fld1;
diff --git a/tests/test_API_env.v b/tests/test_API_env.v
index b1bd25e6e..7519057f7 100644
--- a/tests/test_API_env.v
+++ b/tests/test_API_env.v
@@ -191,7 +191,7 @@ Elpi Query lp:{{
            lp:t lp:y true }})
        , constructor "K2x" (parameter "y" _ {{nat}} y\ arity {{
            lp:t lp:y false }}) ]),
-  coq.typecheck-indt-decl D ok,
+  std.assert-ok! (coq.typecheck-indt-decl D) "illtyped",
   coq.env.add-indt D _.
 }}.
 
diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v
index 5f0779409..381e78921 100644
--- a/tests/test_HOAS.v
+++ b/tests/test_HOAS.v
@@ -624,3 +624,17 @@ Elpi Accumulate  lp:{{
 }}.
 Elpi Comm Class c {A : Type} (x : A -> A).
 Goal c S. Abort.
+
+Elpi Query lp:{{
+  coq.typecheck-ty (sort (typ X)) A ok,
+  A = typ TX,
+  not(coq.univ.alg-super X TX),
+  coq.say X ":" TX,
+  @keep-alg-univs! => coq.typecheck-ty (sort (typ Y)) B ok,
+  B = typ TY,
+  coq.say Y ":" TY,
+  coq.univ.alg-super Y TY,
+  coq.say Y ":" TY
+  .
+
+}}.
\ No newline at end of file