diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml
deleted file mode 100644
index d7b930e871..0000000000
--- a/.github/workflows/macos.yml
+++ /dev/null
@@ -1,166 +0,0 @@
-# Main doc: https://docs.github.com/en/free-pro-team@latest/actions/learn-github-actions/introduction-to-github-actions
-# Runners spec: https://docs.github.com/en/free-pro-team@latest/actions/reference/specifications-for-github-hosted-runners
-# Glob expressions: https://github.com/actions/toolkit/tree/main/packages/glob
-
-name: Macos
-
-###############################################################################
-# Schedule:
-# - push on any branch whose name matches v** or master
-# - any pull request
-###############################################################################
-on:
-  push:
-    branches:
-      - 2021.02
-      - 2021.09
-      - main
-  pull_request:
-    branches:
-      - '**'
-  schedule:
-    - cron: "0 0 * * *"
-  workflow_dispatch:
-    inputs:
-      platform:
-        description: 'Arguments for the platform script:'
-        required: true
-        default: '-extent=f -parallel=p -jobs=2 -vst=y -compcert=y -set-switch=y'
-
-###############################################################################
-# Platform script options shared among all jobs
-###############################################################################
-env:
-  PLATFORM_ARGS: -extent=f -parallel=p -jobs=2 -vst=y -compcert=y -set-switch=y
-  COQREGTESTING: y
-
-###############################################################################
-# Macos
-#
-# CAVEATS:
-# - COQREGTESTING broken, it makes the script loop, so we install opam by hand
-###############################################################################
-jobs:
-  Macos_platform:
-    name: Macos
-    runs-on: macos-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        variant:
-          - '8.15~2022.03'
-          - '8.14~2022.01'
-
-    steps:
-      - name: Git checkout
-        uses: actions/checkout@v2
-
-      - name: Set PLATFORM
-        if: ${{ github.event.inputs.platform != '' }}
-        run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV
-
-      - name: Install opam
-        env:
-          OPAM_VERSION: 2.0.7
-        run: |
-          curl -L https://github.com/ocaml/opam/releases/download/${OPAM_VERSION}/opam-${OPAM_VERSION}-x86_64-macos > opam.${OPAM_VERSION}
-          chmod a+x opam.${OPAM_VERSION}
-          sudo cp opam.${OPAM_VERSION} /usr/local/bin/opam.${OPAM_VERSION}
-          sudo ln -s /usr/local/bin/opam.${OPAM_VERSION} /usr/local/bin/opam
-
-      - name: Run common platform script
-        shell: bash
-        run: ./coq_platform_make.sh -packages=${{matrix.variant}} $PLATFORM_ARGS -dumplogs
-
-      - name: Install bash (needed by smoke scripts)
-        run: brew install bash
-
-      - name: Create smoke test kit
-        shell: bash
-        run: |
-          eval $(opam env)
-          shell_scripts/create_smoke_test_kit.sh
-
-      - name: 'Upload smoke test kit'
-        uses: actions/upload-artifact@v2
-        with:
-          name: 'Smoke Test Kit Macos ${{matrix.variant}}'
-          path: smoke-test-kit/
-          retention-days: 5
-
-      - name: Install findutils, coreutils and macpack (needed by DMG script)
-        run: |
-          brew install findutils
-          brew install coreutils
-          brew install python@3.8
-          pip3 install macpack
-
-      - name: 'Build DMG installer'
-        shell: bash
-        run: |
-          eval $(opam env)
-          macos/create_installer_macos.sh
-
-      - name: 'Upload DMG script logs on failure'
-        uses: actions/upload-artifact@v2
-        if: failure()
-        with:
-          name: 'DMG script error logs ${{matrix.variant}}'
-          path: macos_installer/logs/
-
-      - name: 'Upload Artifact'
-        uses: actions/upload-artifact@v2
-        with:
-          name: 'Macos installer ${{matrix.variant}}'
-          path: macos_installer/coq-*-installer-macos.dmg
-          retention-days: 5
-
-  Macos_smoke:
-    name: Smoke test Macos
-    needs: Macos_platform
-    runs-on: macos-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        variant:
-          - '8.15~2022.03'
-          - '8.14~2022.01'
-
-    steps:
-      - name: Install bash
-        run: brew install bash
-
-      - name: 'Download Artifact'
-        uses: actions/download-artifact@v2
-        id: download
-        with:
-          name: 'Macos installer ${{matrix.variant}}'
-
-      - name: 'Download smoke test kit'
-        uses: actions/download-artifact@v2
-        id: download-smoke
-        with:
-          name: 'Smoke Test Kit Macos ${{matrix.variant}}'
-
-      - name: 'Run Installer'
-        shell: bash
-        run: |
-          cd ${{steps.download.outputs.download-path}}
-          DMG=$(ls coq-*-installer-macos.dmg)
-          hdiutil attach $DMG
-          cp -r /Volumes/${DMG%%.dmg}/Coq_*.app /Applications/
-          hdiutil detach /Volumes/${DMG%%.dmg}/
-
-      - name: 'Smoke coqc'
-        shell: bash
-        run: |
-          cd /Applications/Coq_*.app/Contents/Resources/bin/
-          ./coqc -v
-
-      - name: 'Run Macos smoke test kit'
-        shell: bash
-        run: |
-          export PATH="$PATH:$(cd /Applications/Coq_*.app/Contents/Resources/bin/; pwd)"
-          cd ${{steps.download-smoke.outputs.download-path}}
-          chmod a+x ./run-smoke-test.sh
-          ./run-smoke-test.sh
diff --git a/.github/workflows/mega-linter.yml b/.github/workflows/mega-linter.yml
new file mode 100644
index 0000000000..6be4e2ae8c
--- /dev/null
+++ b/.github/workflows/mega-linter.yml
@@ -0,0 +1,82 @@
+---
+# MegaLinter GitHub Action configuration file
+# More info at https://megalinter.github.io
+name: MegaLinter
+
+on:
+  # Trigger mega-linter at every push. Action will also be visible from Pull Requests to master
+  push: # Comment this line to trigger action only on pull-requests (not recommended if you don't pay for GH Actions)
+  pull_request:
+    branches: [master, main]
+
+env: # Comment env block if you do not want to apply fixes
+  # Apply linter fixes configuration
+  APPLY_FIXES: all # When active, APPLY_FIXES must also be defined as environment variable (in github/workflows/mega-linter.yml or other CI tool)
+  APPLY_FIXES_EVENT: pull_request # Decide which event triggers application of fixes in a commit or a PR (pull_request, push, all)
+  APPLY_FIXES_MODE: commit # If APPLY_FIXES is used, defines if the fixes are directly committed (commit) or posted in a PR (pull_request)
+
+concurrency:
+  group: ${{ github.ref }}-${{ github.workflow }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    name: MegaLinter
+    runs-on: ubuntu-latest
+    steps:
+      # Git Checkout
+      - name: Checkout Code
+        uses: actions/checkout@v2
+        with:
+          token: ${{ secrets.PAT_LINT_SPELL }}
+          fetch-depth: 0
+
+      # MegaLinter
+      - name: MegaLinter
+        id: ml
+        # You can override MegaLinter flavor used to have faster performances
+        # More info at https://megalinter.github.io/flavors/
+        uses: megalinter/megalinter/flavors/python@v5
+        env:
+          # All available variables are described in documentation
+          # https://megalinter.github.io/configuration/
+          VALIDATE_ALL_CODEBASE: true # Set ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' }} to validate only diff with main branch
+          GITHUB_TOKEN: ${{ secrets.PAT_LINT_SPELL }}
+          # ADD YOUR CUSTOM ENV VARIABLES HERE TO OVERRIDE VALUES OF .mega-linter.yml AT THE ROOT OF YOUR REPOSITORY
+
+      # Upload MegaLinter artifacts
+      - name: Archive production artifacts
+        if: ${{ success() }} || ${{ failure() }}
+        uses: actions/upload-artifact@v2
+        with:
+          name: MegaLinter reports
+          path: |
+            report
+            mega-linter.log
+
+      # Create pull request if applicable (for now works only on PR from same repository, not from forks)
+      - name: Create Pull Request with applied fixes
+        id: cpr
+        if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'pull_request' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix')
+        uses: peter-evans/create-pull-request@v3
+        with:
+          token: ${{ secrets.PAT_LINT_SPELL }}
+          commit-message: "[MegaLinter] Apply linters automatic fixes"
+          title: "[MegaLinter] Apply linters automatic fixes"
+          labels: bot
+      - name: Create PR output
+        if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'pull_request' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix')
+        run: |
+          echo "Pull Request Number - ${{ steps.cpr.outputs.pull-request-number }}"
+          echo "Pull Request URL - ${{ steps.cpr.outputs.pull-request-url }}"
+
+      # Push new commit if applicable (for now works only on PR from same repository, not from forks)
+      - name: Prepare commit
+        if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'commit' && github.ref != 'refs/heads/main' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix')
+        run: sudo chown -Rc $UID .git/
+      - name: Commit and push applied linter fixes
+        if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'commit' && github.ref != 'refs/heads/main' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix')
+        uses: stefanzweifel/git-auto-commit-action@v4
+        with:
+          branch: ${{ github.event.pull_request.head.ref || github.head_ref || github.ref }}
+          commit_message: "[MegaLinter] Apply linters fixes"
diff --git a/.github/workflows/ubuntu.yml b/.github/workflows/ubuntu.yml
deleted file mode 100644
index d3ffaefca0..0000000000
--- a/.github/workflows/ubuntu.yml
+++ /dev/null
@@ -1,180 +0,0 @@
-# Main doc: https://docs.github.com/en/free-pro-team@latest/actions/learn-github-actions/introduction-to-github-actions
-# Runners spec: https://docs.github.com/en/free-pro-team@latest/actions/reference/specifications-for-github-hosted-runners
-# Glob expressions: https://github.com/actions/toolkit/tree/main/packages/glob
-
-name: Ubuntu
-
-###############################################################################
-# Schedule:
-# - push on any branch whose name matches v** or master
-# - any pull request
-###############################################################################
-on:
-  push:
-    branches:
-      - 2021.02
-      - 2021.09
-      - main
-  pull_request:
-    branches:
-      - '**'
-  schedule:
-    - cron: "0 0 * * *"
-  workflow_dispatch:
-    inputs:
-      platform:
-        description: 'Arguments for the platform script:'
-        required: true
-        default: '-extent=f -parallel=p -jobs=2 -vst=y -compcert=y -set-switch=y'
-      snap_pick:
-        description: 'Package pick for the snap package:'
-        default: 8.14~2022.01
-      upload:
-        description: 'Upload artifact to Snap Store? (true/false, default false)'
-        default: false
-
-###############################################################################
-# Platform script options shared among all jobs
-###############################################################################
-env:
-  PLATFORM: -extent=f -parallel=p -jobs=2 -vst=y -compcert=y -set-switch=y
-  COQREGTESTING: y
-  SNAP_PICK: 8.14~2022.01
-
-###############################################################################
-# Ubuntu
-#
-# CAVEATS:
-# - you need bubblewrap or the script fails
-# - build-essential pulls in the C toolchain
-###############################################################################
-jobs:
-  Ubuntu_platform:
-    name: Ubuntu
-    runs-on: ubuntu-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        variant:
-          - '8.15~2022.03'
-          - '8.14~2022.01'
-          - '8.13~2021.02'
-          - '8.12'
-
-    steps:
-      - name: Git checkout
-        uses: actions/checkout@v2
-
-      - name: Set PLATFORM
-        if: ${{ github.event.inputs.platform != '' }}
-        run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV
-
-      - name: Install bubblewrap and build-essential
-        run: |
-          sudo apt-get update
-          sudo apt-get install bubblewrap build-essential
-
-      - name: Run common platform script
-        shell: bash
-        run: ./coq_platform_make.sh  -packages=${{matrix.variant}} $PLATFORM -dumplogs
-
-      - name: Create smoke test kit
-        shell: bash
-        run: |
-          eval $(opam env)
-          shell_scripts/create_smoke_test_kit.sh
-
-      - name: 'Run Linux smoke test kit'
-        shell: bash
-        run: |
-          eval $(opam env)
-          smoke-test-kit/run-smoke-test.sh
-
-      - name: 'Upload smoke test kit'
-        uses: actions/upload-artifact@v2
-        with:
-          name: 'Smoke Test Kit ${{matrix.variant}}'
-          path: smoke-test-kit
-          retention-days: 5
-
-  Ubuntu_snap:
-    name: Snap package
-    runs-on: ubuntu-latest
-
-    steps:
-      - name: Git checkout
-        uses: actions/checkout@v2
-
-      - name: Set PLATFORM
-        if: ${{ github.event.inputs.platform != '' }}
-        run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV
-
-      - name: Set SNAP_PICK
-        if: ${{ github.event.inputs.snap_pick != '' }}
-        run: echo "SNAP_PICK=${{ github.event.inputs.snap_pick }}" >> $GITHUB_ENV
-
-      - name: Generate snapcraft file
-        run: linux/create_snapcraft_yaml.sh -packages=$SNAP_PICK $PLATFORM
-
-      - name: Print snapcraft file
-        run: cat snap/snapcraft.yaml
-
-      - name: Run snapcraft
-        uses: snapcore/action-build@v1.0.9
-        id: build
-
-      - name: Save Artifact
-        uses: actions/upload-artifact@v2
-        with:
-          name: 'Snap package'
-          path: ${{ steps.build.outputs.snap }}
-
-      - name: Upload Artifact to the Snap Store
-        if: ${{ github.event.inputs.upload }}
-        uses: snapcore/action-publish@v1
-        with:
-          store_login: ${{ secrets.STORE_LOGIN }}
-          snap: ${{ steps.build.outputs.snap }}
-          release: edge
-
-  # We run this one always because the Ubuntu_platform job
-  # has a matrix and contains the flaky dev job
-  # but here we really only need the SNAP_PICK one
-  #
-  # In any case the job will fail fast if it can't download
-  # the snap or the smoke test
-  Ubuntu_smoke:
-    name: Snap package smoke test
-    if: ${{ always() }}
-    needs: [Ubuntu_platform, Ubuntu_snap]
-    runs-on: ubuntu-latest
-
-    steps:
-
-      - name: Set SNAP_PICK
-        if: ${{ github.event.inputs.snap_pick != '' }}
-        run: echo "SNAP_PICK=${{ github.event.inputs.snap_pick }}" >> $GITHUB_ENV
-
-      - name: Download Artifact
-        uses: actions/download-artifact@v2
-        id: download-snap
-        with:
-          name: 'Snap package'
-
-      - name: 'Download smoke test kit'
-        uses: actions/download-artifact@v2
-        id: download-smoke
-        with:
-          name: 'Smoke Test Kit ${{ env.SNAP_PICK }}'
-
-      - name: 'Install Snap'
-        run: |
-          sudo snap install --dangerous ${{ steps.download-snap.outputs.download-path }}/coq-prover_*.snap
-          sudo snap alias coq-prover.coqc coqc
-
-      - name: 'Run Smoke Test Kit'
-        run: |
-          cd ${{steps.download-smoke.outputs.download-path}}
-          chmod a+x ./run-smoke-test.sh
-          ./run-smoke-test.sh
-          
\ No newline at end of file
diff --git a/.github/workflows/windows.yml b/.github/workflows/windows.yml
deleted file mode 100644
index e00b7c9a48..0000000000
--- a/.github/workflows/windows.yml
+++ /dev/null
@@ -1,142 +0,0 @@
-# Main doc: https://docs.github.com/en/free-pro-team@latest/actions/learn-github-actions/introduction-to-github-actions
-# Runners spec: https://docs.github.com/en/free-pro-team@latest/actions/reference/specifications-for-github-hosted-runners
-# Glob expressions: https://github.com/actions/toolkit/tree/main/packages/glob
-
-name: Windows
-
-###############################################################################
-# Schedule:
-# - push on any branch whose name matches v** or master
-# - any pull request
-###############################################################################
-on:
-  push:
-    branches:
-      - 2021.02
-      - 2021.09
-      - main
-  pull_request:
-    branches:
-      - '**'
-  schedule:
-    - cron: "0 0 * * *"
-  workflow_dispatch:
-    inputs:
-      platform:
-        description: 'Arguments for the platform script:'
-        required: true
-        default: '-extent=f -parallel=p -jobs=2 -vst=y -compcert=y -set-switch=y'
-
-###############################################################################
-# Platform script options shared among all jobs
-###############################################################################
-env:
-  PLATFORM_ARGS: -extent=f -parallel=p -jobs=2 -vst=y -compcert=y -set-switch=y
-  COQREGTESTING: y
-
-###############################################################################
-# Windows
-#
-# 2 jobs, the former builds the installer, the second tests it
-#
-# CAVEATS:
-# - git is misconfigured, by default it puts \r in between \n\n
-###############################################################################
-jobs:
-  Windows_platform:
-    name: Windows
-    runs-on: windows-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        architecture:
-          - '32'
-          - '64'
-        variant:
-          # Keep this in sync with the Smoke test below
-          - '8.15~2022.03'
-          - '8.14~2022.01'
-
-    steps:
-      - name: Set git to use LF
-        run: |
-          git config --global core.autocrlf false
-          git config --global core.eol lf
-
-      - name: Git checkout
-        uses: actions/checkout@v2
-
-      - name: Set PLATFORM
-        if: ${{ github.event.inputs.platform != '' }}
-        run: echo "PLATFORM=${{ github.event.inputs.platform }}" >> $GITHUB_ENV
-
-      - name: Run common platform script
-        shell: cmd
-        run: coq_platform_make_windows.bat -destcyg=C:\cygwin_coq_platform -arch=${{matrix.architecture}} -packages=${{matrix.variant}} %PLATFORM_ARGS% -dumplogs
-
-      - name: Create installer
-        shell: cmd
-        run: C:\cygwin_coq_platform\bin\bash --login -c "cd coq-platform/ && windows/create_installer_windows.sh && mkdir /cygdrive/c/installer && cp windows_installer/*exe /cygdrive/c/installer/"
-
-      - name: Create smoke test kit
-        shell: cmd
-        run: C:\cygwin_coq_platform\bin\bash --login -c "cd coq-platform/ && shell_scripts/create_smoke_test_kit.sh && mkdir /cygdrive/c/smoke && cp -ra smoke-test-kit/* /cygdrive/c/smoke/"
-
-      - name: 'Upload Artifact'
-        uses: actions/upload-artifact@v2
-        with:
-          name: 'Windows installer ${{matrix.variant}} ${{matrix.architecture}}'
-          path: C:\installer\*.exe
-          retention-days: 5
-
-      - name: 'Upload smoke test kit'
-        uses: actions/upload-artifact@v2
-        with:
-          name: 'Smoke Test Kit Windows ${{matrix.variant}} ${{matrix.architecture}}'
-          path: C:\smoke\
-          retention-days: 5
-
-  Windows_smoke:
-    name: Smoke test Windows
-    needs: Windows_platform
-    runs-on: windows-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        architecture:
-          - '32'
-          - '64'
-        variant:
-          - '8.15~2022.03'
-          - '8.14~2022.01'
-
-    steps:
-      - name: 'Download Artifact'
-        uses: actions/download-artifact@v2
-        id: download
-        with:
-          name: 'Windows installer ${{matrix.variant}} ${{matrix.architecture}}'
-
-      - name: 'Download smoke test kit'
-        uses: actions/download-artifact@v2
-        id: download-smoke
-        with:
-          name: 'Smoke Test Kit Windows ${{matrix.variant}} ${{matrix.architecture}}'
-
-      - name: 'Run Installer'
-        shell: cmd
-        run: |
-          cd ${{steps.download.outputs.download-path}}
-          FOR %%f IN (*.exe) DO %%f /S /D=C:\Coq
-
-      - name: 'Smoke coqc'
-        shell: cmd
-        run: C:\Coq\bin\coqc.exe -v
-
-      - name: 'Run Windows smoke test kit'
-        shell: cmd
-        run: |
-          CD ${{steps.download-smoke.outputs.download-path}}
-          DIR
-          SET PATH=C:\Coq\bin\;%PATH%
-          CALL run-smoke-test.bat
diff --git a/.markdown-link-check.json b/.markdown-link-check.json
new file mode 100644
index 0000000000..ecf5d634e5
--- /dev/null
+++ b/.markdown-link-check.json
@@ -0,0 +1,8 @@
+{
+    "replacementPatterns": [
+        {
+            "pattern": "^/",
+            "replacement": "{{BASEURL}}/"
+        }
+    ]
+}
diff --git a/.mega-linter.yml b/.mega-linter.yml
new file mode 100644
index 0000000000..35ba2a8d82
--- /dev/null
+++ b/.mega-linter.yml
@@ -0,0 +1,19 @@
+# Configuration file for MegaLinter
+# See all available variables at https://megalinter.github.io/configuration/ and in linters documentation
+
+APPLY_FIXES: all # all, none, or list of linter keys
+# ENABLE: # If you use ENABLE variable, all other languages/formats/tooling-formats will be disabled by default
+# ENABLE_LINTERS: # If you use ENABLE_LINTERS variable, all other linters will be disabled by default
+DISABLE:
+  - COPYPASTE # Comment to enable checks of excessive copy-pastes
+  # - SPELL # Uncomment to disable checks of spelling mistakes
+DISABLE_LINTERS:
+  - SPELL_CSPELL
+  - ACTION_ACTIONLINT
+  - BASH_SHELLCHECK
+  - C_CPPLINT
+  - BASH_SHFMT
+  - MARKDOWN_MARKDOWNLINT
+SHOW_ELAPSED_TIME: false
+FILEIO_REPORTER: false
+# DISABLE_ERRORS: true # Uncomment if you want MegaLinter to detect errors but not block CI to pass
diff --git a/doc/README_Linux.md b/doc/README_Linux.md
index 779c59f63e..68cd72870d 100755
--- a/doc/README_Linux.md
+++ b/doc/README_Linux.md
@@ -77,7 +77,7 @@ This method is intended for experienced users, who may want to use opam to insta
   - Debian, Ubuntu:       sudo apt-get install build-essential
   - CentOS, RHEL, Fedora: sudo dnf groupinstall "Development Tools"
   - OpenSuse:             sudo zypper in -t pattern devel_C_C++
-- For CentOS and possibly RHEL some additional steps are required, see [CentOS](#centos) below.
+- For CentOS and possibly RHEL some additional steps are required, see [CentOS](#centos-enable-sudo-for-current-user) below.
 - Get the Coq Platform scripts via either of these methods
   - Most users should download and extract `https://github.com/coq/platform/archive/refs/tags/2022.01.0.zip`.
   - Users which intend to contribute to Coq Platform should use `git clone --branch 2022.01.0 https://github.com/coq/platform.git`.
diff --git a/doc/README_macOS.md b/doc/README_macOS.md
index 5f8e0dbc72..a5ab908b28 100644
--- a/doc/README_macOS.md
+++ b/doc/README_macOS.md
@@ -22,8 +22,6 @@ right click the `Coq_Platform` app in `/Applications` in Finder and select `open
 - In case you want to use the installed `coqc` from the command line, please add the folder `/Applications/Coq_Platform_2022.01.0.app/Contents/Resources/bin` to your `PATH`.
 - If you want to inspect the installed content, right click the `Coq_Platform` app in `/Applications` in Finder and select `Show Package Contents`.
 
-A note to lecturers: it is easy to create a customized Windows installer from an opam switch - see [Customized Installers](#customized-installers)
-
 # Installation by compiling from Sources using opam
 
 This method is intended for experienced users, who may want to use opam to install additional packages, beyond the standard set provided by the Coq Platform.
diff --git a/doc/README~8.12.md b/doc/README~8.12.md
index c9c594947c..e95448e147 100644
--- a/doc/README~8.12.md
+++ b/doc/README~8.12.md
@@ -98,7 +98,7 @@ developments.
 
 The packages in the **full level** are mature, well maintained
 and suitable as basis for your own developments.
-See the Coq Platform [charter](charter.md) for details.
+See the Coq Platform [charter](../charter.md) for details.
 
 The **full level** contains the following packages:
 
diff --git a/doc/README~8.13~2021.02.md b/doc/README~8.13~2021.02.md
index c46d2ea3d7..6303a7a639 100644
--- a/doc/README~8.13~2021.02.md
+++ b/doc/README~8.13~2021.02.md
@@ -98,7 +98,7 @@ developments.
 
 The packages in the **full level** are mature, well maintained
 and suitable as basis for your own developments.
-See the Coq Platform [charter](charter.md) for details.
+See the Coq Platform [charter](../charter.md) for details.
 
 The **full level** contains the following packages:
 
@@ -248,7 +248,7 @@ The **full level** contains the following packages:
       (<a href='https://github.com/HoTT/HoTT/issues'>bug reports</a>)
       (<a href='https://coq.inria.fr/opam/released/packages/coq-hott/coq-hott.8.13/opam'>opam package</a>)
     </dd>
-    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:<br>   -noinit -indices-matter<br>To use the HoTT library in a project, add the following to _CoqProject:<br>   -arg -noinit<br>   -arg -indices-matter</dd>
+    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:<br>   -noinit -indices-matter<br>To use the HoTT library in a project, add the following to <code>_CoqProject</code>:<br>   -arg -noinit<br>   -arg -indices-matter</dd>
   </dl>
 </details>
 
diff --git a/doc/README~8.13~2021.09.md b/doc/README~8.13~2021.09.md
index 31327af485..6be0b6ee01 100644
--- a/doc/README~8.13~2021.09.md
+++ b/doc/README~8.13~2021.09.md
@@ -98,7 +98,7 @@ developments.
 
 The packages in the **full level** are mature, well maintained
 and suitable as basis for your own developments.
-See the Coq Platform [charter](charter.md) for details.
+See the Coq Platform [charter](../charter.md) for details.
 
 The **full level** contains the following packages:
 
diff --git a/doc/README~8.13~2022.01.md b/doc/README~8.13~2022.01.md
index 8b74e2540e..94120387e3 100644
--- a/doc/README~8.13~2022.01.md
+++ b/doc/README~8.13~2022.01.md
@@ -98,7 +98,7 @@ developments.
 
 The packages in the **full level** are mature, well maintained
 and suitable as basis for your own developments.
-See the Coq Platform [charter](charter.md) for details.
+See the Coq Platform [charter](../charter.md) for details.
 
 The **full level** contains the following packages:
 
diff --git a/doc/README~8.14~2022.01.md b/doc/README~8.14~2022.01.md
index 6e8a098cc2..e33c947fc8 100644
--- a/doc/README~8.14~2022.01.md
+++ b/doc/README~8.14~2022.01.md
@@ -98,7 +98,7 @@ developments.
 
 The packages in the **full level** are mature, well maintained
 and suitable as basis for your own developments.
-See the Coq Platform [charter](charter.md) for details.
+See the Coq Platform [charter](../charter.md) for details.
 
 The **full level** contains the following packages:
 
@@ -353,7 +353,7 @@ The **full level** contains the following packages:
       (<a href='https://github.com/HoTT/HoTT/issues'>bug reports</a>)
       (<a href='https://coq.inria.fr/opam/released/packages/coq-hott/coq-hott.8.14/opam'>opam package</a>)
     </dd>
-    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:<br>   -noinit -indices-matter<br>To use the HoTT library in a project, add the following to _CoqProject:<br>   -arg -noinit<br>   -arg -indices-matter</dd>
+    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:<br>   -noinit -indices-matter<br>To use the HoTT library in a project, add the following to <code>_CoqProject</code>:<br>   -arg -noinit<br>   -arg -indices-matter</dd>
   </dl>
 </details>
 
diff --git a/doc/README~8.15~2022.03.md b/doc/README~8.15~2022.03.md
index 8ecd849a94..a5805aab2c 100644
--- a/doc/README~8.15~2022.03.md
+++ b/doc/README~8.15~2022.03.md
@@ -98,7 +98,7 @@ developments.
 
 The packages in the **full level** are mature, well maintained
 and suitable as basis for your own developments.
-See the Coq Platform [charter](charter.md) for details.
+See the Coq Platform [charter](../charter.md) for details.
 
 The **full level** contains the following packages:
 
@@ -353,7 +353,7 @@ The **full level** contains the following packages:
       (<a href='https://github.com/HoTT/HoTT/issues'>bug reports</a>)
       (<a href='https://coq.inria.fr/opam/released/packages/coq-hott/coq-hott.8.15/opam'>opam package</a>)
     </dd>
-    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:<br>   -noinit -indices-matter<br>To use the HoTT library in a project, add the following to _CoqProject:<br>   -arg -noinit<br>   -arg -indices-matter</dd>
+    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:<br>   -noinit -indices-matter<br>To use the HoTT library in a project, add the following to <code>_CoqProject</code>:<br>   -arg -noinit<br>   -arg -indices-matter</dd>
   </dl>
 </details>
 
diff --git a/doc/README~dev.md b/doc/README~dev.md
index abc8e27b2a..10b33d4533 100644
--- a/doc/README~dev.md
+++ b/doc/README~dev.md
@@ -98,7 +98,7 @@ developments.
 
 The packages in the **full level** are mature, well maintained
 and suitable as basis for your own developments.
-See the Coq Platform [charter](charter.md) for details.
+See the Coq Platform [charter](../charter.md) for details.
 
 The **full level** contains the following packages:
 
@@ -350,7 +350,7 @@ The **full level** contains the following packages:
       (<a href='https://github.com/HoTT/HoTT/issues'>bug reports</a>)
       (<a href='https://coq.inria.fr/opam/extra-dev/packages/coq-hott/coq-hott.dev/opam'>opam package</a>)
     </dd>
-    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:n   -noinit -indices-matternnTo use the HoTT library in a project, add the following to _CoqProject:n   -arg -noinitn   -arg -indices-mattern`</dd>
+    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:n   -noinit -indices-matternnTo use the HoTT library in a project, add the following to <code>_CoqProject</code>:n   -arg -noinitn   -arg -indices-mattern`</dd>
   </dl>
 </details>