diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index f503da8..65d0246 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -19,13 +19,9 @@ jobs:
     strategy:
       matrix:
         image:
-          - mathcomp/mathcomp:2.1.0-coq-8.16
-          - mathcomp/mathcomp:2.1.0-coq-8.17
-          - mathcomp/mathcomp:2.1.0-coq-8.18
+          - mathcomp/mathcomp:2.1.0-coq-8.20
           - mathcomp/mathcomp:2.1.0-coq-dev
-          - mathcomp/mathcomp-dev:coq-8.16
-          - mathcomp/mathcomp-dev:coq-8.17
-          - mathcomp/mathcomp-dev:coq-8.18
+          - mathcomp/mathcomp-dev:coq-8.20
           - mathcomp/mathcomp-dev:coq-dev
       fail-fast: false
     steps:
diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml
deleted file mode 100644
index 9bab485..0000000
--- a/.github/workflows/nix-action-8.18.yml
+++ /dev/null
@@ -1,254 +0,0 @@
-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@v4
-      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@v4
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v30
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v15
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepGetDerivation
-      name: Getting derivation for current job (coq)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.18\" --argstr job \"coq\" \\\n   --dry-run 2> err > out || (touch fail;
-        true)\n"
-    - name: Error reporting
-      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
-    - name: Failure check
-      run: if [ -e fail ]; then exit 1; else exit 0; fi;
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.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@v4
-      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@v4
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v30
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v15
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepGetDerivation
-      name: Getting derivation for current job (mathcomp)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.18\" --argstr job \"mathcomp\" \\\n   --dry-run 2> err > out || (touch
-        fail; true)\n"
-    - name: Error reporting
-      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
-    - name: Failure check
-      run: if [ -e fail ]; then exit 1; else exit 0; fi;
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
-        job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: stdlib'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
-        job "stdlib"
-    - 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 previous CI target: stdlib'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
-        job "stdlib"
-    - 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"
-  odd-order:
-    needs:
-    - coq
-    - mathcomp
-    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@v4
-      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@v4
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v30
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v15
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepGetDerivation
-      name: Getting derivation for current job (odd-order)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.18\" --argstr job \"odd-order\" \\\n   --dry-run 2> err > out || (touch
-        fail; true)\n"
-    - name: Error reporting
-      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
-    - name: Failure check
-      run: if [ -e fail ]; then exit 1; else exit 0; fi;
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
-        job "coq"
-    - 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: 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'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
-        job "mathcomp"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: stdlib'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
-        job "stdlib"
-    - 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 "odd-order"
-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:
-    - master
diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml
deleted file mode 100644
index 84ddf27..0000000
--- a/.github/workflows/nix-action-8.19.yml
+++ /dev/null
@@ -1,254 +0,0 @@
-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@v4
-      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@v4
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v30
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v15
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepGetDerivation
-      name: Getting derivation for current job (coq)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.19\" --argstr job \"coq\" \\\n   --dry-run 2> err > out || (touch fail;
-        true)\n"
-    - name: Error reporting
-      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
-    - name: Failure check
-      run: if [ -e fail ]; then exit 1; else exit 0; fi;
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.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@v4
-      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@v4
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v30
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v15
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepGetDerivation
-      name: Getting derivation for current job (mathcomp)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.19\" --argstr job \"mathcomp\" \\\n   --dry-run 2> err > out || (touch
-        fail; true)\n"
-    - name: Error reporting
-      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
-    - name: Failure check
-      run: if [ -e fail ]; then exit 1; else exit 0; fi;
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
-        job "coq"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: stdlib'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
-        job "stdlib"
-    - 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 previous CI target: stdlib'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
-        job "stdlib"
-    - 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"
-  odd-order:
-    needs:
-    - coq
-    - mathcomp
-    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@v4
-      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@v4
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v30
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v15
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq, coq-community
-        name: math-comp
-    - id: stepGetDerivation
-      name: Getting derivation for current job (odd-order)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"8.19\" --argstr job \"odd-order\" \\\n   --dry-run 2> err > out || (touch
-        fail; true)\n"
-    - name: Error reporting
-      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
-    - name: Failure check
-      run: if [ -e fail ]; then exit 1; else exit 0; fi;
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
-        job "coq"
-    - 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: 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'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
-        job "mathcomp"
-    - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: stdlib'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
-        job "stdlib"
-    - 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 "odd-order"
-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:
-    - master
diff --git a/.nix/config.nix b/.nix/config.nix
index e3b107b..3544210 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -35,14 +35,6 @@
   ## write one `bundles.name` attribute set per
   ## alternative configuration, the can be used to
   ## compute several ci jobs as well
-  bundles."8.18".coqPackages = {
-    coq.override.version = "8.18";
-    mathcomp.override.version = "mathcomp-2.1.0";
-  };
-  bundles."8.19".coqPackages = {
-    coq.override.version = "8.19";
-    mathcomp.override.version = "mathcomp-2.2.0";
-  };
   bundles."8.20".coqPackages = {
     coq.override.version = "8.20";
     mathcomp.override.version = "mathcomp-2.2.0";
diff --git a/coq-mathcomp-odd-order.opam b/coq-mathcomp-odd-order.opam
index b343316..ccc8ba5 100644
--- a/coq-mathcomp-odd-order.opam
+++ b/coq-mathcomp-odd-order.opam
@@ -13,7 +13,7 @@ install: [ make "install" ]
 depends: [
   "ocaml"
   "coq-mathcomp-character" { (>= "2.0.0") | (= "dev") }
-  "coq" { >= "8.18" }
+  "coq" { >= "8.20" }
 ]
 tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
 authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
diff --git a/theories/BGsection1.v b/theories/BGsection1.v
index 9d20d82..a098e23 100644
--- a/theories/BGsection1.v
+++ b/theories/BGsection1.v
@@ -105,24 +105,20 @@ Definition Puig_inf (gT : finGroupType) (G : {set gT}) := Puig_at #|G|.*2 G.
 
 Definition Puig (gT : finGroupType) (G : {set gT}) := Puig_at #|G|.*2.+1 G.
 
-Notation "p .-length_1" := (plength_1 p)
-  (at level 2, format "p .-length_1") : group_scope.
+Notation "p .-length_1" := (plength_1 p) (format "p .-length_1") : group_scope.
 
 Notation "p .-constrained" := (p_constrained p)
-  (at level 2, format "p .-constrained") : group_scope.
+  (format "p .-constrained") : group_scope.
 Notation "p .-abelian_constrained" := (p_abelian_constrained p)
-  (at level 2, format "p .-abelian_constrained") : group_scope.
-Notation "p .-stable" := (p_stable p)
-  (at level 2, format "p .-stable") : group_scope.
+  (format "p .-abelian_constrained") : group_scope.
+Notation "p .-stable" := (p_stable p) (format "p .-stable") : group_scope.
 
 Notation "''L_[' G ] ( L )" := (Puig_succ G L)
-  (at level 8, format  "''L_[' G ] ( L )") : group_scope.
+  (format  "''L_[' G ] ( L )") : group_scope.
 Notation "''L_{' n } ( G )" := (Puig_at n G)
-  (at level 8, format "''L_{' n } ( G )") : group_scope.
-Notation "''L_*' ( G )" := (Puig_inf G)
-  (at level 8, format "''L_*' ( G )") : group_scope.
-Notation "''L' ( G )" := (Puig G)
-  (at level 8, format "''L' ( G )") : group_scope.
+  (format "''L_{' n } ( G )") : group_scope.
+Notation "''L_*' ( G )" := (Puig_inf G) (format "''L_*' ( G )") : group_scope.
+Notation "''L' ( G )" := (Puig G) (format "''L' ( G )") : group_scope.
 
 Section BGsection1.
 
@@ -1250,7 +1246,7 @@ End PuigSeriesGroups.
 
 Notation "''L_[' G ] ( L )" := (Puig_succ_group G L) : Group_scope.
 Notation "''L_{' n } ( G )" := (Puig_at_group n G)
-  (at level 8, format "''L_{' n } ( G )") : Group_scope.
+  (format "''L_{' n } ( G )") : Group_scope.
 Notation "''L_*' ( G )" := (Puig_inf_group G) : Group_scope.
 Notation "''L' ( G )" := (Puig_group G) : Group_scope.
 
diff --git a/theories/BGsection10.v b/theories/BGsection10.v
index f00023d..e3101db 100644
--- a/theories/BGsection10.v
+++ b/theories/BGsection10.v
@@ -32,9 +32,9 @@ Unset Printing Implicit Defensive.
 
 Import GroupScope.
 
-Reserved Notation "\alpha ( M )" (at level 2, format "\alpha ( M )").
-Reserved Notation "\beta ( M )" (at level 2, format "\beta ( M )").
-Reserved Notation "\sigma ( M )" (at level 2, format "\sigma ( M )").
+Reserved Notation "\alpha ( M )" (format "\alpha ( M )").
+Reserved Notation "\beta ( M )" (format "\beta ( M )").
+Reserved Notation "\sigma ( M )" (format "\sigma ( M )").
 
 Reserved Notation "M `_ \alpha" (at level 3, format "M `_ \alpha").
 Reserved Notation "M `_ \beta" (at level 3, format "M `_ \beta").
diff --git a/theories/BGsection12.v b/theories/BGsection12.v
index 7b055f4..8bc4870 100644
--- a/theories/BGsection12.v
+++ b/theories/BGsection12.v
@@ -45,12 +45,9 @@ Definition sigma_complement E E1 E2 E3 :=
 
 End Definitions.
 
-Notation "\tau1 ( M )" := (tau1 M)
-  (at level 2, format "\tau1 ( M )") : group_scope.
-Notation "\tau2 ( M )" := (tau2 M)
-  (at level 2, format "\tau2 ( M )") : group_scope.
-Notation "\tau3 ( M )" := (tau3 M)
-  (at level 2, format "\tau3 ( M )") : group_scope.
+Notation "\tau1 ( M )" := (tau1 M) (format "\tau1 ( M )") : group_scope.
+Notation "\tau2 ( M )" := (tau2 M) (format "\tau2 ( M )") : group_scope.
+Notation "\tau3 ( M )" := (tau3 M) (format "\tau3 ( M )") : group_scope.
 
 Section Section12.
 
diff --git a/theories/BGsection14.v b/theories/BGsection14.v
index 22d4bc3..0f056fe 100644
--- a/theories/BGsection14.v
+++ b/theories/BGsection14.v
@@ -115,43 +115,40 @@ Definition TypeP2_maxgroups := TypeP_maxgroups :\: TypeP1_maxgroups.
 End Definitons.
 
 Notation "\ell_ \sigma ( x )" := (sigma_length x)
-  (at level 8, format "\ell_ \sigma ( x )") : group_scope.
+  (format "\ell_ \sigma ( x )") : group_scope.
 
 Notation "''M_' \sigma ( X )" := (sigma_mmax_of X)
-  (at level 8, format "''M_' \sigma ( X )") : group_scope.
+  (format "''M_' \sigma ( X )") : group_scope.
 
 Notation "''M_' \sigma [ x ]" := (sigma_mmax_of <[x]>)
-  (at level 8, format "''M_' \sigma [ x ]") : group_scope.
+  (format "''M_' \sigma [ x ]") : group_scope.
 
 Notation "''N' [ x ]" := (FT_signalizer_base x)
-  (at level 8, format "''N' [ x ]") : group_scope.
+  (format "''N' [ x ]") : group_scope.
 
 Notation "''R' [ x ]" := (FT_signalizer x)
-  (at level 8, format "''R' [ x ]") : group_scope.
+  (format "''R' [ x ]") : group_scope.
 
-Notation "M ^~~" := (sigma_cover M)
-  (at level 2, format "M ^~~") : group_scope.
+Notation "M ^~~" := (sigma_cover M) (format "M ^~~") : group_scope.
 
-Notation "\tau13 ( M )" := (tau13 M)
-  (at level 8, format "\tau13 ( M )") : group_scope.
+Notation "\tau13 ( M )" := (tau13 M) (format "\tau13 ( M )") : group_scope.
 
-Notation "\kappa ( M )" := (kappa M)
-  (at level 8, format "\kappa ( M )") : group_scope.
+Notation "\kappa ( M )" := (kappa M) (format "\kappa ( M )") : group_scope.
 
 Notation "\sigma_kappa ( M )" := (sigma_kappa M)
-  (at level 8, format "\sigma_kappa ( M )") : group_scope.
+  (format "\sigma_kappa ( M )") : group_scope.
 
 Notation "''M_' ''F'" := (TypeF_maxgroups _)
-  (at level 2, format "''M_' ''F'") : group_scope.
+  (format "''M_' ''F'") : group_scope.
 
 Notation "''M_' ''P'" := (TypeP_maxgroups _)
-  (at level 2, format "''M_' ''P'") : group_scope.
+  (format "''M_' ''P'") : group_scope.
 
 Notation "''M_' ''P1'" := (TypeP1_maxgroups _)
-  (at level 2, format "''M_' ''P1'") : group_scope.
+  (format "''M_' ''P1'") : group_scope.
 
 Notation "''M_' ''P2'" := (TypeP2_maxgroups _)
-  (at level 2, format "''M_' ''P2'") : group_scope.
+  (format "''M_' ''P2'") : group_scope.
 
 Section Section14.
 
diff --git a/theories/BGsection16.v b/theories/BGsection16.v
index 2a768a5..1188b79 100644
--- a/theories/BGsection16.v
+++ b/theories/BGsection16.v
@@ -198,14 +198,11 @@ End Definitions.
 Notation "M `_ \s" := (FTcore M) (at level 3, format "M `_ \s") : group_scope.
 Notation "M `_ \s" := (FTcore_group M) : Group_scope.
 
-Notation "''A1' ( M )" := (FTsupport1 M)
-  (at level 8, format "''A1' ( M )") : group_scope.
+Notation "''A1' ( M )" := (FTsupport1 M) (format "''A1' ( M )") : group_scope.
 
-Notation "''A' ( M )" := (FTsupport M)
-  (at level 8, format "''A' ( M )") : group_scope.
+Notation "''A' ( M )" := (FTsupport M) (format "''A' ( M )") : group_scope.
 
-Notation "''A0' ( M )" := (FTsupport0 M)
-  (at level 8, format "''A0' ( M )") : group_scope.
+Notation "''A0' ( M )" := (FTsupport0 M) (format "''A0' ( M )") : group_scope.
 
 Notation "''M^' G" := (mmax_transversal G)
   (at level 3, format "''M^' G") : group_scope.
diff --git a/theories/BGsection2.v b/theories/BGsection2.v
index 88b72cf..4df8456 100644
--- a/theories/BGsection2.v
+++ b/theories/BGsection2.v
@@ -221,11 +221,9 @@ Let E2_ i t :=
 Local Notation "''V_' i" := (V_ i) (at level 8, i at level 2, format "''V_' i").
 Local Notation "''n_' i" := (n_ i) (at level 8, i at level 2, format "''n_' i").
 Local Notation "''E_' i" := (E_ i) (at level 8, i at level 2, format "''E_' i").
-Local Notation "'E_ ( i )" := (E_ i) (at level 8, only parsing).
-Local Notation "e ^g" := (g^-1 *m (e *m g))
-  (at level 8, format "e ^g") : ring_scope.
-Local Notation "'E_ ( i , t )" := (E2_ i t)
-  (at level 8, format "''E_' ( i ,  t )").
+Local Notation "'E_ ( i )" := (E_ i) (only parsing).
+Local Notation "e ^g" := (g^-1 *m (e *m g)) (format "e ^g") : ring_scope.
+Local Notation "'E_ ( i , t )" := (E2_ i t) (format "''E_' ( i ,  t )").
 
 Let inj_g : g \in GRing.unit.
 Proof. by rewrite -(unitrX_pos _ h_gt0) gh1 unitr1. Qed.
diff --git a/theories/BGsection5.v b/theories/BGsection5.v
index 0f895ed..7493fa2 100644
--- a/theories/BGsection5.v
+++ b/theories/BGsection5.v
@@ -37,7 +37,7 @@ Unset Printing Implicit Defensive.
 
 Import GroupScope.
 
-Reserved Notation "p .-narrow" (at level 2, format "p .-narrow").
+Reserved Notation "p .-narrow" (format "p .-narrow").
 
 Section Definitions.
 
diff --git a/theories/BGsection7.v b/theories/BGsection7.v
index dcf44e3..f71d809 100644
--- a/theories/BGsection7.v
+++ b/theories/BGsection7.v
@@ -44,15 +44,13 @@ Unset Printing Implicit Defensive.
 
 Import GroupScope.
 
-Reserved Notation "''M'" (at level 8, format "''M'").
-Reserved Notation "''M' ( H )" (at level 8, format "''M' ( H )").
-Reserved Notation "''U'" (at level 8).
-Reserved Notation "''SCN_' n [ p ]"
-  (at level 8, n at level 2, format "''SCN_' n [ p ]").
+Reserved Notation "''M'" (format "''M'").
+Reserved Notation "''M' ( H )" (format "''M' ( H )").
+Reserved Notation "''U'".
+Reserved Notation "''SCN_' n [ p ]" (n at level 2, format "''SCN_' n [ p ]").
 Reserved Notation "|/|_ X ( A ; pi )"
-  (at level 8, X at level 2, format "|/|_ X ( A ;  pi )").
-Reserved Notation "|/|* ( A ; pi )"
-  (at level 8, format "|/|* ( A ;  pi )").
+  (X at level 2, format "|/|_ X ( A ;  pi )").
+Reserved Notation "|/|* ( A ; pi )" (format "|/|* ( A ;  pi )").
 
 (* The generic setup for the whole Odd Order Theorem proof. *)
 
diff --git a/theories/PFsection10.v b/theories/PFsection10.v
index 2f48dcf..d0188ea 100644
--- a/theories/PFsection10.v
+++ b/theories/PFsection10.v
@@ -52,7 +52,7 @@ Local Notation G := (TheMinSimpleOddGroup gT).
 Implicit Types (p q : nat) (x y z : gT).
 Implicit Types H K L N P Q R S T U W : {group gT}.
 
-Local Notation "#1" := (inord 1) (at level 0).
+Local Notation "#1" := (inord 1).
 
 Section OneMaximal.
 
@@ -64,15 +64,15 @@ Variables M U_M W W1 W2 : {group gT}.
 Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W).
 Hypotheses (MtypeP : of_typeP M U_M defW) (notMtype2: FTtype M != 2).
 
-Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
+Local Notation "` 'M'" := (gval M) (only parsing) : group_scope.
+Local Notation "` 'W1'" := (gval W1) (only parsing) : group_scope.
+Local Notation "` 'W2'" := (gval W2) (only parsing) : group_scope.
+Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation V := (cyclicTIset defW).
 Local Notation M' := M^`(1)%G.
-Local Notation "` 'M''" := `M^`(1) (at level 0) : group_scope.
+Local Notation "` 'M''" := `M^`(1) : group_scope.
 Local Notation M'' := M^`(2)%G.
-Local Notation "` 'M'''" := `M^`(2) (at level 0) : group_scope.
+Local Notation "` 'M'''" := `M^`(2) : group_scope.
 
 Let defM : M' ><| W1 = M. Proof. by have [[]] := MtypeP. Qed.
 Let nsM''M' : M'' <| M'. Proof. exact: (der_normal 1 M'). Qed.
@@ -389,8 +389,7 @@ Section NonCoherence.
 Variable tau1 : {additive 'CF(M) -> 'CF(G)}.
 Hypothesis cohS : coherent_with calS M^# tau tau1.
 
-Local Notation "mu ^\tau1" := (tau1 mu%CF)
-  (at level 2, format "mu ^\tau1") : ring_scope.
+Local Notation "mu ^\tau1" := (tau1 mu%CF) (format "mu ^\tau1") : ring_scope.
 
 Let Dtau1 : {in 'Z[calS, M'^#], tau1 =1 tau}.
 Proof. by case: cohS => _; apply: sub_in1; apply: zchar_onS; apply: setSD. Qed.
@@ -876,9 +875,9 @@ by rewrite expr1n big1 ?addr0 // => j1 _; rewrite Da a_j normCK !mul0r.
 Qed.
 
 Local Notation H := M'.
-Local Notation "` 'H'" := `M' (at level 0) : group_scope.
+Local Notation "` 'H'" := `M' : group_scope.
 Local Notation H' := M''.
-Local Notation "` 'H''" := `M'' (at level 0) : group_scope.
+Local Notation "` 'H''" := `M'' : group_scope.
 
 (* This is the bulk of the proof of Peterfalvi, Theorem (10.10); as with      *)
 (* (10.8), it will be restated below in order to remove dependencies on zeta, *)
diff --git a/theories/PFsection11.v b/theories/PFsection11.v
index 502be74..eb9ce04 100644
--- a/theories/PFsection11.v
+++ b/theories/PFsection11.v
@@ -66,24 +66,24 @@ Qed.
 Let Mtype_gt2 : (FTtype M > 2)%N. Proof. by case/pred2P: Mtype34 => ->. Qed.
 
 Local Notation H0 := (Ptype_Fcore_kernel MtypeP).
-Local Notation "` 'H0'" := (gval H0) (at level 0, only parsing) : group_scope.
-Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope.
-Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
+Local Notation "` 'H0'" := (gval H0) (only parsing) : group_scope.
+Local Notation "` 'M'" := (gval M) (only parsing) : group_scope.
+Local Notation "` 'U'" := (gval U) (only parsing) : group_scope.
+Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
+Local Notation "` 'W1'" := (gval W1) (only parsing) : group_scope.
+Local Notation "` 'W2'" := (gval W2) (only parsing) : group_scope.
 Local Notation H := `M`_\F%G.
-Local Notation "` 'H'" := `M`_\F (at level 0) : group_scope.
+Local Notation "` 'H'" := `M`_\F : group_scope.
 Local Notation HU := M^`(1)%G.
-Local Notation "` 'HU'" := `M^`(1)%g (at level 0) : group_scope.
+Local Notation "` 'HU'" := `M^`(1)%g : group_scope.
 Local Notation U' := U^`(1)%G.
-Local Notation "` 'U''" := `U^`(1)%g (at level 0) : group_scope.
+Local Notation "` 'U''" := `U^`(1)%g : group_scope.
 Local Notation C := 'C_U(`H)%G.
-Local Notation "` 'C'" := 'C_`U(`H) (at level 0) : group_scope.
+Local Notation "` 'C'" := 'C_`U(`H) : group_scope.
 Local Notation HC := (`H <*> `C)%G.
-Local Notation "` 'HC'" := (`H <*> `C) (at level 0) : group_scope.
+Local Notation "` 'HC'" := (`H <*> `C) : group_scope.
 Local Notation H0C := (`H0 <*> `C)%G.
-Local Notation "` 'H0C'" := (`H0 <*> `C) (at level 0) : group_scope.
+Local Notation "` 'H0C'" := (`H0 <*> `C) : group_scope.
 Local Notation Hbar := (`H / `H0)%g.
 
 Local Notation S_ := (seqIndD HU M HU).
diff --git a/theories/PFsection12.v b/theories/PFsection12.v
index d8fcddb..2e726dc 100644
--- a/theories/PFsection12.v
+++ b/theories/PFsection12.v
@@ -39,9 +39,9 @@ Variable L : {group gT}.
 
 Hypotheses (maxL : L \in 'M) (Ltype1 : FTtype L == 1%N).
 
-Local Notation "` 'L'" := (gval L) (at level 0, only parsing) : group_scope.
+Local Notation "` 'L'" := (gval L) (only parsing) : group_scope.
 Local Notation H := `L`_\F%G.
-Local Notation "` 'H'" := `L`_\F (at level 0) : group_scope.
+Local Notation "` 'H'" := `L`_\F : group_scope.
 
 Let nsHL : H <| L. Proof. exact: gFnormal. Qed.
 Let calS := seqIndD H L H 1%G.
@@ -305,11 +305,11 @@ Section Twelve_4_to_6.
 Variable L : {group gT}.
 Hypothesis maxL : L \in 'M .
 
-Local Notation "` 'L'" := (gval L) (at level 0, only parsing) : group_scope.
+Local Notation "` 'L'" := (gval L) (only parsing) : group_scope.
 Local Notation H := `L`_\F%G.
-Local Notation "` 'H'" := `L`_\F (at level 0) : group_scope.
+Local Notation "` 'H'" := `L`_\F : group_scope.
 Local Notation H' := H^`(1)%G.
-Local Notation "` 'H''" := `H^`(1) (at level 0) : group_scope.
+Local Notation "` 'H''" := `H^`(1) : group_scope.
 
 Let calS := seqIndD H L H 1%G.
 Let tau := FT_Dade maxL.
@@ -625,7 +625,7 @@ Hypotheses (P0_1s_x : x \in 'Ohm_1(P0)^#) (not_sCxK' : ~~ ('C_K[x] \subset K')).
 Hypotheses (sNxM : 'N(<[x]>) \subset M) (not_sCxL : ~~ ('C[x] \subset L)).
 
 Let H := L`_\F%G.
-Local Notation "` 'H'" := (gval L)`_\F (at level 0, format "` 'H'").
+Local Notation "` 'H'" := (gval L)`_\F (format "` 'H'").
 Let nsHL : H <| L. Proof. exact: gFnormal. Qed.
 
 (* This is Peterfalvi (12.10). *)
diff --git a/theories/PFsection13.v b/theories/PFsection13.v
index 98621a4..c063389 100644
--- a/theories/PFsection13.v
+++ b/theories/PFsection13.v
@@ -59,7 +59,7 @@ Implicit Types H K L N P Q R S T U W : {group gT}.
 Definition irr_Ind_Fitting S := [predI irr S & seqIndT 'F(S) S].
 
 Local Notation irrIndH := (irr_Ind_Fitting _).
-Local Notation "#1" := (inord 1) (at level 0).
+Local Notation "#1" := (inord 1).
 
 Section Thirteen_2_3_5_to_9.
 
@@ -78,21 +78,21 @@ Variables S U W W1 W2 : {group gT}.
 Hypotheses (maxS : S \in 'M) (defW : W1 \x W2 = W).
 Hypotheses (StypeP : of_typeP S U defW).
 
-Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
+Local Notation "` 'W1'" := (gval W1) (only parsing) : group_scope.
+Local Notation "` 'W2'" := (gval W2) (only parsing) : group_scope.
+Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation V := (cyclicTIset defW).
 
-Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
+Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
 Local Notation P := `S`_\F%G.
-Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
+Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
-Local Notation "` 'PU'" := `S^`(1) (at level 0) : group_scope.
-Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
+Local Notation "` 'PU'" := `S^`(1) : group_scope.
+Local Notation "` 'U'" := (gval U) (only parsing) : group_scope.
 Local Notation C := 'C_U(`P)%G.
-Local Notation "` 'C'" := 'C_`U(`P) (at level 0) : group_scope.
+Local Notation "` 'C'" := 'C_`U(`P) : group_scope.
 Local Notation H := 'F(S)%G.
-Local Notation "` 'H'" := 'F(`S) (at level 0) : group_scope.
+Local Notation "` 'H'" := 'F(`S) : group_scope.
 
 Let defS : PU ><| W1 = S. Proof. by have [[]] := StypeP. Qed.
 Let defPU : P ><| U = PU. Proof. by have [_ []] := StypeP. Qed.
@@ -868,21 +868,21 @@ Variables S U W W1 W2 : {group gT}.
 Hypotheses (maxS : S \in 'M) (defW : W1 \x W2 = W).
 Hypotheses (StypeP : of_typeP S U defW).
 
-Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
+Local Notation "` 'W1'" := (gval W1) (only parsing) : group_scope.
+Local Notation "` 'W2'" := (gval W2) (only parsing) : group_scope.
+Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation V := (cyclicTIset defW).
 
-Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
+Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
 Local Notation P := `S`_\F%G.
-Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
+Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
-Local Notation "` 'PU'" := `S^`(1) (at level 0) : group_scope.
-Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
+Local Notation "` 'PU'" := `S^`(1) : group_scope.
+Local Notation "` 'U'" := (gval U) (only parsing) : group_scope.
 Local Notation C := 'C_U(`P)%G.
-Local Notation "` 'C'" := 'C_`U(`P) (at level 0) : group_scope.
+Local Notation "` 'C'" := 'C_`U(`P) : group_scope.
 Local Notation H := 'F(S)%G.
-Local Notation "` 'H'" := 'F(`S) (at level 0) : group_scope.
+Local Notation "` 'H'" := 'F(`S) : group_scope.
 
 Let defS : PU ><| W1 = S. Proof. by have [[]] := StypeP. Qed.
 Let defPU : P ><| U = PU. Proof. by have [_ []] := StypeP. Qed.
@@ -1584,17 +1584,17 @@ Variables S U W W1 W2 : {group gT}.
 Hypotheses (maxS : S \in 'M) (defW : W1 \x W2 = W).
 Hypotheses (StypeP : of_typeP S U defW).
 
-Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
+Local Notation "` 'W1'" := (gval W1) (only parsing) : group_scope.
+Local Notation "` 'W2'" := (gval W2) (only parsing) : group_scope.
+Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation V := (cyclicTIset defW).
 
-Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
+Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
 Local Notation P := `S`_\F%G.
-Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
+Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
-Local Notation "` 'PU'" := `S^`(1) (at level 0) : group_scope.
-Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
+Local Notation "` 'PU'" := `S^`(1) : group_scope.
+Local Notation "` 'U'" := (gval U) (only parsing) : group_scope.
 
 Let defS : PU ><| W1 = S. Proof. by have [[]] := StypeP. Qed.
 Let defPU : P ><| U = PU. Proof. by have [_ []] := StypeP. Qed.
@@ -1949,9 +1949,9 @@ Qed.
 Variable L : {group gT}.
 Hypotheses (maxL : L \in 'M) (Ltype1 : FTtype L == 1%N).
 
-Local Notation "` 'L'" := (gval L) (at level 0, only parsing) : group_scope.
+Local Notation "` 'L'" := (gval L) (only parsing) : group_scope.
 Local Notation H := `L`_\F%G.
-Local Notation "` 'H'" := `L`_\F (at level 0) : group_scope.
+Local Notation "` 'H'" := `L`_\F : group_scope.
 
 Let e :=  #|L : H|.
 Let tauL := FT_DadeF maxL.
diff --git a/theories/PFsection14.v b/theories/PFsection14.v
index ac73785..dced02d 100644
--- a/theories/PFsection14.v
+++ b/theories/PFsection14.v
@@ -36,7 +36,7 @@ Local Notation G := (TheMinSimpleOddGroup gT).
 Implicit Types (p q : nat) (x y z : gT).
 Implicit Types H K L N P Q R S T U W : {group gT}.
 
-Local Notation "#1" := (inord 1) (at level 0).
+Local Notation "#1" := (inord 1).
 
 (* Supplementary results that apply to both S and T, but that are not         *)
 (* formally stated as such; T, V, L, tau1L and phi are only used at the end   *)
@@ -50,14 +50,14 @@ Variables (tau1L : {additive 'CF(L) -> 'CF(G)}) (phi : 'CF(L)).
 (* Implicit (dependent) forward assuptions. *)
 Hypotheses (defW : W1 \x W2 = W) (xdefW : W2 \x W1 = W) (maxL : L \in 'M).
 
-Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
+Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
 Local Notation P := `S`_\F%G.
-Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
+Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
-Local Notation "` 'PU'" := `S^`(1)%g (at level 0) : group_scope.
-Local Notation "` 'L'" := (gval L) (at level 0, only parsing).
+Local Notation "` 'PU'" := `S^`(1)%g : group_scope.
+Local Notation "` 'L'" := (gval L) (only parsing).
 Local Notation H := `L`_\F%G.
-Local Notation "` 'H'" := `L`_\F%g (at level 0, format "` 'H'") : group_scope.
+Local Notation "` 'H'" := `L`_\F%g (format "` 'H'") : group_scope.
 
 Let p := #|W2|.
 Let q := #|W1|.
@@ -375,24 +375,24 @@ Hypotheses (defW : W1 \x W2 = W) (xdefW : W2 \x W1 = W).
 Hypotheses (pairST : typeP_pair S T defW) (maxS : S \in 'M) (maxT : T \in 'M).
 Hypotheses (StypeP : of_typeP S U defW) (TtypeP : of_typeP T V xdefW).
 
-Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
+Local Notation "` 'W1'" := (gval W1) (only parsing) : group_scope.
+Local Notation "` 'W2'" := (gval W2) (only parsing) : group_scope.
+Local Notation "` 'W'" := (gval W) (only parsing) : group_scope.
 Local Notation What := (cyclicTIset defW).
 
-Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
+Local Notation "` 'S'" := (gval S) (only parsing) : group_scope.
 Local Notation P := `S`_\F%G.
-Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
+Local Notation "` 'P'" := `S`_\F : group_scope.
 Local Notation PU := S^`(1)%G.
-Local Notation "` 'PU'" := `S^`(1) (at level 0) : group_scope.
-Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
+Local Notation "` 'PU'" := `S^`(1) : group_scope.
+Local Notation "` 'U'" := (gval U) (only parsing) : group_scope.
 
-Local Notation "` 'T'" := (gval T) (at level 0, only parsing) : group_scope.
+Local Notation "` 'T'" := (gval T) (only parsing) : group_scope.
 Local Notation Q := `T`_\F%G.
-Local Notation "` 'Q'" := `T`_\F (at level 0) : group_scope.
+Local Notation "` 'Q'" := `T`_\F : group_scope.
 Local Notation QV := T^`(1)%G.
-Local Notation "` 'QV'" := `T^`(1) (at level 0) : group_scope.
-Local Notation "` 'V'" := (gval V) (at level 0, only parsing) : group_scope.
+Local Notation "` 'QV'" := `T^`(1) : group_scope.
+Local Notation "` 'V'" := (gval V) (only parsing) : group_scope.
 
 Let defS : PU ><| W1 = S. Proof. by have [[]] := StypeP. Qed.
 Let defPU : P ><| U = PU. Proof. by have [_ []] := StypeP. Qed.
@@ -492,9 +492,9 @@ Let Stype2 := FTtypeP_max_typeII.
 
 (* These correspond to Peterfalvi, Hypothesis (14.3). *)
 Variables (L : {group gT}) (tau1L : {additive 'CF(L) -> 'CF(G)}) (phi : 'CF(L)).
-Local Notation "` 'L'" := (gval L) (at level 0, only parsing).
+Local Notation "` 'L'" := (gval L) (only parsing).
 Local Notation H := `L`_\F%G.
-Local Notation "` 'H'" := `L`_\F%g (at level 0, format "` 'H'") : group_scope.
+Local Notation "` 'H'" := `L`_\F%g (format "` 'H'") : group_scope.
 
 Hypothesis maxNU_L : L \in 'M('N(U)).
 
@@ -856,9 +856,9 @@ Let Ttype2 := FTtypeP_min_typeII.
 Variables (M : {group gT}) (tau1M : {additive 'CF(M) -> 'CF(G)}) (psi : 'CF(M)).
 Hypothesis maxNV_M : M \in 'M('N(V)).
 
-Local Notation "` 'M'" := (gval M) (at level 0, only parsing).
+Local Notation "` 'M'" := (gval M) (only parsing).
 Local Notation K := `M`_\F%G.
-Local Notation "` 'K'" := `M`_\F%g (at level 0, format "` 'K'") : group_scope.
+Local Notation "` 'K'" := `M`_\F%g (format "` 'K'") : group_scope.
 
 (* Consequences of the above. *)
 Hypotheses (maxM : M \in 'M) (sNVM : 'N(V) \subset M).
diff --git a/theories/PFsection2.v b/theories/PFsection2.v
index d1ed67d..0c13e2d 100644
--- a/theories/PFsection2.v
+++ b/theories/PFsection2.v
@@ -49,7 +49,7 @@ Unset Printing Implicit Defensive.
 Import GroupScope GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
-Reserved Notation "alpha ^\tau" (at level 2, format "alpha ^\tau").
+Reserved Notation "alpha ^\tau" (format "alpha ^\tau").
 
 Section Two.
 
@@ -419,11 +419,11 @@ Qed.
 
 Definition Dade_set_signalizer (B : {set gT}) := \bigcap_(a in B) H a.
 Local Notation "''H' ( B )" := (Dade_set_signalizer B)
-  (at level 8, format "''H' ( B )") : group_scope.
+  (format "''H' ( B )") : group_scope.
 Canonical Dade_set_signalizer_group B := [group of 'H(B)].
 Definition Dade_set_normalizer B := 'H(B) <*> 'N_L(B).
 Local Notation "''M' ( B )" := (Dade_set_normalizer B)
-  (at level 8, format "''M' ( B )") : group_scope.
+  (format "''M' ( B )") : group_scope.
 Canonical Dade_set_normalizer_group B := [group of 'M(B)].
 
 Let calP := [set B : {set gT} | B \subset A & B != set0].
diff --git a/theories/PFsection3.v b/theories/PFsection3.v
index d9be5f2..cfa8132 100644
--- a/theories/PFsection3.v
+++ b/theories/PFsection3.v
@@ -201,7 +201,7 @@ Notation x7 := +x7. Notation x8 := +x8.
 Definition AndLit kvs kv := kv :: kvs.
 Definition AddLit := AndLit.
 Declare Scope defclause_scope.
-Notation "(*dummy*)" := (Prop Prop) (at level 0) : defclause_scope.
+Notation "(*dummy*)" := (Prop Prop) : defclause_scope.
 Arguments AddLit _%defclause_scope _.
 Infix "+" := AddLit : defclause_scope.
 Definition SubLit kvs kv := AddLit kvs (kv.1, - kv.2).
diff --git a/theories/PFsection7.v b/theories/PFsection7.v
index 5d1b99c..c155b17 100644
--- a/theories/PFsection7.v
+++ b/theories/PFsection7.v
@@ -31,7 +31,7 @@ Unset Printing Implicit Defensive.
 Import GroupScope Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
-Reserved Notation "alpha ^\rho" (at level 2, format "alpha ^\rho").
+Reserved Notation "alpha ^\rho" (format "alpha ^\rho").
 
 Section Seven.
 
diff --git a/theories/PFsection8.v b/theories/PFsection8.v
index 987538c..6ddfe19 100644
--- a/theories/PFsection8.v
+++ b/theories/PFsection8.v
@@ -59,7 +59,7 @@ Local Open Scope ring_scope.
 
 (* Supercedes the notation in BGsection14. *)
 Notation "''R' [ x ]" := 'C_((gval 'N[x])`_\F)[x]
- (at level 8, format "''R' [ x ]")  : group_scope.
+  (format "''R' [ x ]")  : group_scope.
 Notation "''R' [ x ]" := 'C_('N[x]%g`_\F)[x]%G : Group_scope.
 
 Section Definitions.
@@ -80,14 +80,14 @@ Definition FT_Dade_support M X :=
 End Definitions.
 
 Notation "''R_' M" := (FTsignalizer M)
- (at level 8, M at level 2, format "''R_' M") : group_scope.
+  (at level 8, M at level 2, format "''R_' M") : group_scope.
 
 Notation "''A~' ( M , A )" := (FT_Dade_support M A)
-  (at level 8, format "''A~' ( M ,  A )").
+  (format "''A~' ( M ,  A )").
 
-Notation "''A1~' ( M )" := 'A~(M, 'A1(M)) (at level 8, format "''A1~' ( M )").
-Notation "''A~' ( M )" := 'A~(M, 'A(M)) (at level 8, format "''A~' ( M )").
-Notation "''A0~' ( M )" := 'A~(M, 'A0(M)) (at level 8, format "''A0~' ( M )").
+Notation "''A1~' ( M )" := 'A~(M, 'A1(M)) (format "''A1~' ( M )").
+Notation "''A~' ( M )" := 'A~(M, 'A(M)) (format "''A~' ( M )").
+Notation "''A0~' ( M )" := 'A~(M, 'A0(M)) (format "''A0~' ( M )").
 
 Section Eight.
 
diff --git a/theories/PFsection9.v b/theories/PFsection9.v
index 969cc8a..ab8c53e 100644
--- a/theories/PFsection9.v
+++ b/theories/PFsection9.v
@@ -55,16 +55,16 @@ Variables M U W W1 W2 : {group gT}.
 Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W) (MtypeP: of_typeP M U defW).
 Hypothesis notMtype5 : FTtype M != 5.
 
-Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope.
-Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
-Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
+Local Notation "` 'M'" := (gval M) (only parsing) : group_scope.
+Local Notation "` 'U'" := (gval U) (only parsing) : group_scope.
+Local Notation "` 'W1'" := (gval W1) (only parsing) : group_scope.
 Local Notation H := `M`_\F%G.
-Local Notation "` 'H'" := `M`_\F (at level 0) : group_scope.
-Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
+Local Notation "` 'H'" := `M`_\F : group_scope.
+Local Notation "` 'W2'" := (gval W2) (only parsing) : group_scope.
 Local Notation HU := M^`(1)%G.
-Local Notation "` 'HU'" := `M^`(1) (at level 0) : group_scope.
+Local Notation "` 'HU'" := `M^`(1) : group_scope.
 Local Notation U' := U^`(1)%G.
-Local Notation "` 'U''" := `U^`(1) (at level 0) : group_scope.
+Local Notation "` 'U''" := `U^`(1) : group_scope.
 
 Let q := #|W1|.
 
@@ -147,9 +147,9 @@ Qed.
 Definition Ptype_Fcore_kernel of of_typeP M U defW :=
   odflt 1%G [pick H0 : {group gT} | chief_factor M H0 H & 'C_H(U) \subset H0].
 Let H0 := (Ptype_Fcore_kernel MtypeP).
-Local Notation "` 'H0'" := (gval H0) (at level 0, only parsing) : group_scope.
+Local Notation "` 'H0'" := (gval H0) (only parsing) : group_scope.
 Local Notation Hbar := (H / `H0)%G.
-Local Notation "` 'Hbar'" := (`H / `H0)%g (at level 0) : group_scope.
+Local Notation "` 'Hbar'" := (`H / `H0)%g : group_scope.
 Let p := pdiv #|Hbar|.
 
 (* This corresponds to Peterfalvi (9.4). *)
@@ -191,13 +191,13 @@ Fact Ptype_Fcompl_kernel_key : unit. Proof. by []. Qed.
 Definition Ptype_Fcompl_kernel :=
   locked_with Ptype_Fcompl_kernel_key 'C_U(Hbar | 'Q)%G.
 Local Notation C := Ptype_Fcompl_kernel.
-Local Notation "` 'C'" := (gval C) (at level 0, only parsing) : group_scope.
+Local Notation "` 'C'" := (gval C) (only parsing) : group_scope.
 Local Notation Ubar := (U / `C)%G.
-Local Notation "` 'Ubar'" := (`U / `C)%g (at level 0) : group_scope.
+Local Notation "` 'Ubar'" := (`U / `C)%g : group_scope.
 Local Notation W1bar := (W1 / `H0)%G.
-Local Notation "` 'W1bar'" := (`W1 / `H0)%g (at level 0) : group_scope.
+Local Notation "` 'W1bar'" := (`W1 / `H0)%g : group_scope.
 Local Notation W2bar := 'C_Hbar(`W1bar)%G.
-Local Notation "` 'W2bar'" := 'C_`Hbar(`W1bar) (at level 0) : group_scope.
+Local Notation "` 'W2bar'" := 'C_`Hbar(`W1bar) : group_scope.
 Let c := #|C|.
 Let u := #|Ubar|.
 Local Notation tau := (FT_Dade0 maxM).
@@ -210,13 +210,13 @@ Let S_ Y := seqIndD M^`(1) M M`_\F Y.
 Local Notation inMb := (coset (gval H0)).
 
 Local Notation H0C := (`H0 <*> `C)%G.
-Local Notation "` 'H0C'" := (`H0 <*> `C) (at level 0) : group_scope.
+Local Notation "` 'H0C'" := (`H0 <*> `C) : group_scope.
 Local Notation HC := (`H <*> `C)%G.
-Local Notation "` 'HC'" := (`H <*> `C) (at level 0) : group_scope.
+Local Notation "` 'HC'" := (`H <*> `C) : group_scope.
 Local Notation H0U' := (`H0 <*> `U')%G.
-Local Notation "` 'H0U''" := (gval H0 <*> `U')%G (at level 0) : group_scope.
+Local Notation "` 'H0U''" := (gval H0 <*> `U')%G : group_scope.
 Local Notation H0C' := (`H0 <*> `C^`(1)%g)%G.
-Local Notation "` 'H0C''" := (`H0 <*> `C^`(1)) (at level 0) : group_scope.
+Local Notation "` 'H0C''" := (`H0 <*> `C^`(1)) : group_scope.
 
 Let defW2bar : W2bar :=: W2 / H0.
 Proof.