diff --git a/.github/workflows/alpine.yml b/.github/workflows/alpine.yml
index dafe1fd6b3..ecab993f82 100644
--- a/.github/workflows/alpine.yml
+++ b/.github/workflows/alpine.yml
@@ -35,7 +35,20 @@ jobs:
       with:
         branch: ${{ matrix.alpine }}
         extra-repositories: https://dl-cdn.alpinelinux.org/alpine/edge/testing
-        packages: rocq dune
-    - name: dune build -p rocq-stdlib
+        packages: rocq dune  bash python3 graphviz  make findutils diffutils grep rsync
+    - name: 'dune build @stdlib-html # depends on stdlib'
       shell: alpine.sh {0}
-      run: dune build -p rocq-stdlib
+      run: 'dune build @stdlib-html # depends on stdlib'
+    - name: 'find _build/default/doc/stdlib/html/ -iname "*\**" -print -delete # for upload-artifact'
+      shell: alpine.sh {0}
+      run: 'find _build/default/doc/stdlib/html/ -iname "*\**" -print -delete # for upload-artifact'
+    - uses: actions/upload-artifact@v4
+      with:
+        name: stdlib-html
+        path: _build/default/doc/stdlib/html
+    - name: Check for duplicate files
+      shell: alpine.sh {0}
+      run: dev/tools/check-duplicate-files.sh
+    - name: 'make -j -k test-suite'
+      shell: alpine.sh {0}
+      run: 'make -j -k test-suite'
diff --git a/.github/workflows/basic-checks.yml b/.github/workflows/basic-checks.yml
deleted file mode 100644
index 6eafe6c8fe..0000000000
--- a/.github/workflows/basic-checks.yml
+++ /dev/null
@@ -1,16 +0,0 @@
-name: Basic checks
-on:
-  pull_request:
-  push:
-    branches:
-    - master
-jobs:
-  basic-checks:
-    runs-on: ubuntu-latest
-    steps:
-    - name: Checkout
-      uses: actions/checkout@v4
-    - name: Check for duplicate files
-      run: dev/tools/check-duplicate-files.sh
-    - name: Check that All.v is up to date
-      run: dev/tools/check-all.sh
diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml
index d665f45ea8..9239965201 100644
--- a/.github/workflows/nix-action-rocq-9.0.yml
+++ b/.github/workflows/nix-action-rocq-9.0.yml
@@ -7650,60 +7650,6 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
         --argstr job "stdlib"
-  stdlib-html:
-    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@v31
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup coq
-      uses: cachix/cachix-action@v16
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq-community, math-comp
-        name: coq
-    - id: stepGetDerivation
-      name: Getting derivation for current job (stdlib-html)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"rocq-9.0\" --argstr job \"stdlib-html\" \\\n   --dry-run 2> err > out ||
-        (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting
-        derivation failed\"; exit 1; fi\n"
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: "if $(cat out err | grep -q \"built:\") ; then\n  echo \"CI target needs
-        actual building\"\n  if $(cat out err | grep -q \"derivations will be built:\"\
-        ) ; then\n    echo \"waiting a bit for derivations that should be in cache\"\
-        \n    sleep 30\n  fi\nelse\n  echo \"CI target already built\"\n  echo \"\
-        status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
-        --argstr job "stdlib-html"
   stdlib-refman-html:
     needs:
     - coq
@@ -7768,60 +7714,6 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
         --argstr job "stdlib-refman-html"
-  stdlib-subcomponents:
-    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@v31
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup coq
-      uses: cachix/cachix-action@v16
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq-community, math-comp
-        name: coq
-    - id: stepGetDerivation
-      name: Getting derivation for current job (stdlib-subcomponents)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"rocq-9.0\" --argstr job \"stdlib-subcomponents\" \\\n   --dry-run 2> err
-        > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error:
-        getting derivation failed\"; exit 1; fi\n"
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: "if $(cat out err | grep -q \"built:\") ; then\n  echo \"CI target needs
-        actual building\"\n  if $(cat out err | grep -q \"derivations will be built:\"\
-        ) ; then\n    echo \"waiting a bit for derivations that should be in cache\"\
-        \n    sleep 30\n  fi\nelse\n  echo \"CI target already built\"\n  echo \"\
-        status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
-        --argstr job "stdlib-subcomponents"
   stdlib-test:
     needs: []
     runs-on: ubuntu-latest
diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml
index 2223d238c5..49682777a7 100644
--- a/.github/workflows/nix-action-rocq-master.yml
+++ b/.github/workflows/nix-action-rocq-master.yml
@@ -7038,60 +7038,6 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
         --argstr job "stdlib"
-  stdlib-html:
-    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@v31
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup coq
-      uses: cachix/cachix-action@v16
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq-community, math-comp
-        name: coq
-    - id: stepGetDerivation
-      name: Getting derivation for current job (stdlib-html)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"rocq-master\" --argstr job \"stdlib-html\" \\\n   --dry-run 2> err > out
-        || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting
-        derivation failed\"; exit 1; fi\n"
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: "if $(cat out err | grep -q \"built:\") ; then\n  echo \"CI target needs
-        actual building\"\n  if $(cat out err | grep -q \"derivations will be built:\"\
-        ) ; then\n    echo \"waiting a bit for derivations that should be in cache\"\
-        \n    sleep 30\n  fi\nelse\n  echo \"CI target already built\"\n  echo \"\
-        status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
-        --argstr job "stdlib-html"
   stdlib-refman-html:
     needs:
     - coq
@@ -7156,60 +7102,6 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
         --argstr job "stdlib-refman-html"
-  stdlib-subcomponents:
-    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@v31
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup coq
-      uses: cachix/cachix-action@v16
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq-community, math-comp
-        name: coq
-    - id: stepGetDerivation
-      name: Getting derivation for current job (stdlib-subcomponents)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"rocq-master\" --argstr job \"stdlib-subcomponents\" \\\n   --dry-run 2>
-        err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"\
-        Error: getting derivation failed\"; exit 1; fi\n"
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: "if $(cat out err | grep -q \"built:\") ; then\n  echo \"CI target needs
-        actual building\"\n  if $(cat out err | grep -q \"derivations will be built:\"\
-        ) ; then\n    echo \"waiting a bit for derivations that should be in cache\"\
-        \n    sleep 30\n  fi\nelse\n  echo \"CI target already built\"\n  echo \"\
-        status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master"
-        --argstr job "stdlib-subcomponents"
   stdlib-test:
     needs: []
     runs-on: ubuntu-latest
diff --git a/.gitignore b/.gitignore
index 4eb5c522b0..1bf80881fe 100644
--- a/.gitignore
+++ b/.gitignore
@@ -157,6 +157,9 @@ bin
 # generated by dune build -p
 *.install
 
+# generated by /theories/All.sh in make-based build
+/theories/All.v
+
 .dune-stamp
 theories/dune
 user-contrib/Ltac2/dune
diff --git a/.nix/config.nix b/.nix/config.nix
index 06a3619a3e..df5fa7efb7 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -222,9 +222,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       rocq-elpi.override.version = "master";
       rocq-elpi.override.elpi-version = "2.0.7";
       rocq-elpi-test.override.version = "master";
-      stdlib-html.job = true;
       stdlib-test.job = true;
-      stdlib-subcomponents.job = true;
     };
   in {
     "rocq-master" = { rocqPackages = common-bundles // {
diff --git a/.nix/rocq-overlays/stdlib-html/default.nix b/.nix/rocq-overlays/stdlib-html/default.nix
deleted file mode 100644
index b2bafd34ca..0000000000
--- a/.nix/rocq-overlays/stdlib-html/default.nix
+++ /dev/null
@@ -1,23 +0,0 @@
-{ graphviz, stdlib, rocqPackages }:
-
-rocqPackages.lib.overrideRocqDerivation {
-  pname = "stdlib-html";
-
-  overrideBuildInputs = stdlib.buildInputs ++ [ graphviz ];
-
-  useDune = true;
-
-  buildPhase = ''
-    patchShebangs dev/with-rocq-wrap.sh
-    patchShebangs doc/stdlib/make-library-index
-    dev/with-rocq-wrap.sh dune build @stdlib-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
-    # check that the make-depend script still runs
-    patchShebangs dev/tools/make-depends.sh
-    dev/tools/make-depends.sh
-  '';
-
-  installPhase = ''
-    echo "nothing to install"
-    touch $out
-  '';
-} stdlib
diff --git a/.nix/rocq-overlays/stdlib-subcomponents/default.nix b/.nix/rocq-overlays/stdlib-subcomponents/default.nix
deleted file mode 100644
index da155dcc14..0000000000
--- a/.nix/rocq-overlays/stdlib-subcomponents/default.nix
+++ /dev/null
@@ -1,69 +0,0 @@
-# CI job to test that we don't break the subcomponent structure of the stdlib,
-# as described in the graph doc/stdlib/depends.dot
-
-{ rocq-core, stdlib, rocqPackages }:
-
-let
-  # stdlib subcomponents with their dependencies
-  # when editing this, ensure to keep doc/stdlib/depends.dot in sync
-  components = {
-    "corelib-wrapper" = [ ];
-    "logic" = [ ];
-    "relations" = [ "corelib-wrapper" ];
-    "program" = [ "corelib-wrapper" "logic" ];
-    "classes" = [ "program" "relations" ];
-    "bool" = [ "classes" ];
-    "structures" = [ "bool" ];
-    "arith-base" = [ "structures" ];
-    "positive" = [ "arith-base" ];
-    "narith" = [ "ring" ];
-    "zarith-base" = [ "narith-base" ];
-    "narith-base" = [ "positive" ];
-    "lists" = [ "arith-base" ];
-    "ring" = [ "zarith-base" "lists" ];
-    "arith" = [ "ring" ];
-    "strings" = [ "arith" ];
-    "lia" = [ "arith" "narith" ];
-    "zarith" = [ "lia" ];
-    "zmod" = [ "zarith" "sorting" "field" ];
-    "qarith-base" = [ "ring" ];
-    "field" = [ "zarith" ];
-    "lqa" = [ "field" "qarith-base" ];
-    "qarith" = [ "lqa" ];
-    "classical-logic" = [ "arith" ];
-    "sets" = [ "classical-logic" ];
-    "vectors" = [ "lists" ];
-    "sorting" = [ "lia" "sets" "vectors" ];
-    "orders-ex" = [ "strings" "sorting" ];
-    "unicode" = [ ];
-    "primitive-int" = [ "unicode" "zarith" ];
-    "primitive-floats" = [ "primitive-int" ];
-    "primitive-array" = [ "primitive-int" ];
-    "primitive-string" = [ "primitive-int" "orders-ex" ];
-    "reals" = [ "qarith" "classical-logic" "vectors" ];
-    "fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
-    "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
-    "funind" = [ "arith-base" ];
-    "wellfounded" = [ "lists" ];
-    "streams" = [ "logic" ];
-    "rtauto" = [ "positive" "lists" ];
-    "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "zmod" "wellfounded" "streams" ];
-    "all" = [ "compat" ];
-  };
-
-  stdlib_ = component: let
-    pname = "stdlib-${component}";
-    stdlib-deps = map stdlib_ components.${component};
-    in rocqPackages.lib.overrideRocqDerivation ({
-      inherit pname;
-      propagatedBuildInputs = stdlib-deps;
-      mlPlugin = true;
-    } // {
-      buildPhase = ''
-        make ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} build-${component}
-      '';
-      installPhase = ''
-        make COQLIBINSTALL=$out/lib/coq/${rocq-core.rocq-version}/user-contrib install-${component}
-      '';
-    }) stdlib;
-in stdlib_ "all"
diff --git a/Makefile b/Makefile
index 77f8609f2d..4dffeafa2f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
 DUNE=dev/with-rocq-wrap.sh dune
 
-.PHONY: clean all install dune dune-install
+.PHONY: clean all install dune dune-install test-suite
 
 all install:
 	+$(MAKE) -j -C theories $@
@@ -24,11 +24,11 @@ refman-html:
 stdlib-html:
 	$(DUNE) build --root . @stdlib-html
 
+test-suite:
+	test -d _build/default/theories/
+	+COQEXTRAFLAGS="-Q ../_build/default/theories/ Stdlib" \
+	COQCHKEXTRAFLAGS="$$COQEXTRAFLAGS" \
+	$(MAKE) -C test-suite
+
 clean:
-	rm -rf _build
-	find . \
-	\( -name '*.vo' \
-	-o -name '*.vok' \
-	-o -name '*.vos' \
-	-o -name '*.glob' \
-	\) -exec rm -vf {} +
+	+$(MAKE) -C theories clean
diff --git a/dev/doc/README-CI.md b/dev/doc/README-CI.md
index 52d47cce93..105c2eaa0b 100644
--- a/dev/doc/README-CI.md
+++ b/dev/doc/README-CI.md
@@ -72,20 +72,3 @@ token in the coq-community organization to authenticate and store the
 results. Any CI build is stored globally and can be used on one's own
 computer as described in
 https://github.com/math-comp/math-comp/wiki/Using-nix
-
-### Specific CI jobs
-
-#### stdlib-subcomponents
-
-Checks that the dependencies between stdlib subcomponents (as
-documented in [doc/stdlib/index.html](../../doc/stdlib/index.html)) is
-not broken.
-
-#### Other non-Nix jobs
-
-##### basic-checks
-
-Checks that the theories/Make.all and other theories/Make.* files are
-consistent. Also checks that no two sources files in the stdlib (+ Rocq
-prelude) have the same name (which could lead to conflict when doing
-`From Stdlib Require File.`). Some lint checks are also performed.
diff --git a/dev/doc/structure.md b/dev/doc/structure.md
index 103cdb2b05..680a71cffa 100644
--- a/dev/doc/structure.md
+++ b/dev/doc/structure.md
@@ -18,32 +18,19 @@ help somewhat master that situation.
 Documentation
 -------------
 
-One can find a graph of dependencies in file
-`doc/stdlib/depends.dot`. This graph is included in the documentation
-built by `make stdlib-html` in directory
-`_build/default/doc/stdlib/html/`. To find the exact files contained
-in each node `<n>` of this graph, one can look at the corresponding
-`theories/Make.<n>` file.
-
-CI testing
-----------
-
-A CI job `stdlib-subcomponents` checks that the above documented
-structure remains valid.
+Special `.v` files in `subcomponents/` are used to group the normal `.v` files under `theories/` into subcomponents.
+A file in one subcomponent can only depend on a file in another subcomponent
+if the former file's subcomponent depends on the latter file's subcomponent
+(potentially through other subcomponents).
+This rule, and the completeness of the subcomponent categorization,
+are checked during `make stdlib-html` by `dev/tools/subcomponents.py`,
+generating a dependency graph in `_build/default/doc/stdlib/index-subcomponents.html`.
 
 How to Modify the Structure
 ---------------------------
 
-When adding a file, it is enough to list it in the appropriate
-`theories/Make.*` file. Note that, for historical reasons, some
-directories are split between different subcomponents. In this case,
-the new line in the `theories/Make.*` file must contain the
-appropriate `_SubComponent` fake subdirectory. Look at
-`theories/Make.lists` for an example.
+When adding a file, it is sufficient to list it in the appropriate `subcomponents/*.v` file.
+However, it is often preferable to instead `Require` the new file in an existing `.v` file documented in doc/stdlib/index.html`
+(which is already assigned to the appropriate subcomponent).
 
-To add or remove a subcomponent, just add or remove the corresponding
-`theories/Make.*` file and adapt `doc/stdlib/depends.dot` and
-`.nix/rocq-overlays/stdlib-subcomponents/default.nix`. One can use the
-`dev/tools/make-depends.sh` script to help update the graph (the line
-below `File dependencies` can be uncommented to better understand
-which files are responsible for some subcomponent dependency).
+`dev/tools/subcomponents.py` can be called directly to check that subcomponents are declared consistently and diagnose related issues.
diff --git a/dev/tools/check-all.sh b/dev/tools/check-all.sh
deleted file mode 100755
index 441c9c89a0..0000000000
--- a/dev/tools/check-all.sh
+++ /dev/null
@@ -1,20 +0,0 @@
-#!/bin/sh
-
-# Check that theories/All/All.v is up to date
-
-ALL_FILES=all_files__
-ACTUAL_FILES=actual_files__
-
-rm -f ${ALL_FILES} ${ACTUAL_FILES}
-grep "Require" theories/All/All.v | sed -e 's/From.*Require.*Export.*[.]\([a-zA-Z]\)/\1/' | sort > ${ALL_FILES}
-(for f in $(find theories -name "*.v" -type f) ; do basename ${f%v} ; done) | grep -v "^All[.]$" | sort > ${ACTUAL_FILES}
-
-if $(diff -q ${ALL_FILES} ${ACTUAL_FILES} > /dev/null) ; then
-  echo "theories/All/All.v is up to date."
-else
-  echo "Error: theories/All/All.v needs some update:"
-  diff -u ${ALL_FILES} ${ACTUAL_FILES}
-  exit 1
-fi
-
-rm -f ${ALL_FILES} ${ACTUAL_FILES}
diff --git a/dev/tools/make-depends.sh b/dev/tools/make-depends.sh
deleted file mode 100755
index 5e8965fde2..0000000000
--- a/dev/tools/make-depends.sh
+++ /dev/null
@@ -1,51 +0,0 @@
-#!/bin/bash
-
-# this should be called from root as
-# % dev/tools/make-depends.sh
-
-THEORIES="theories"
-
-declare -A FILE_PKG
-
-# Associate each *.v source file to its corresponding <pkg>,
-# according to theories/Make.<pkg>
-FILE_PKG["All.v"]="all"
-for makefile in theories/Make.* ; do
-    PKG=${makefile#theories/Make.}
-    for f in $(cat ${makefile} | sed -e 's/#.*//;s/-.*//' | grep -v '^[ \t]*$') ; do
-        f=$(echo ${f} | sed -e 's,/_[^/]*,,')
-        if [ -n ${FILE_PKG[${f}]:-""} ] ; then
-            echo "Error: File ${f} appears in both theories/Make.${FILE_PKG[${f}]} and theories/Make.${PKG}."
-            exit 1
-        fi
-        FILE_PKG[${f}]=${PKG}
-    done
-done
-
-# Check that each *.v file in theories appears in some <pkg>
-for f in $(find ${THEORIES} -name "*.v") ; do
-    f=$(echo ${f} | sed -e "s,${THEORIES}/,,")
-    if [ -z ${FILE_PKG[${f}]} ] ; then
-        echo "Error: File ${f} is not listed in any theories/Make.* file."
-        exit 1
-    fi
-done
-
-# Retrieve dependencies and build graph
-(echo "digraph stdlib_deps {";
-echo "node [shape=rectangle, style=filled, color=\"#ff540a\", URL=\"#\\N\"];";
-rocq dep -Q ${THEORIES} Stdlib ${THEORIES} | sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*v//p' | \
-    while read src dst; do
-        src=${src#theories.}
-        srcf="$(echo ${src%.vo} | tr '.' '/').v"
-        for d in $dst; do
-            d=${d#theories.}
-            df="$(echo ${d%.vo} | tr '.' '/').v"
-            if [ -z ${FILE_PKG[${df}]:-""} ] ; then continue ; fi
-            # File dependencies
-            # echo "\"(${src}) ${FILE_PKG[${srcf}]}\" -> \"${FILE_PKG[${df}]} (${d%.vo})\" ;"
-            # Subcomponent dependencies
-            echo "\"${FILE_PKG[${srcf}]}\" -> \"${FILE_PKG[${df}]}\" ;"
-        done
-    done
-echo "}") | tred
diff --git a/dev/tools/subcomponents.py b/dev/tools/subcomponents.py
new file mode 100755
index 0000000000..b81691730d
--- /dev/null
+++ b/dev/tools/subcomponents.py
@@ -0,0 +1,112 @@
+import sys, os, functools
+from glob import glob
+from subprocess import Popen, PIPE, STDOUT
+
+vs = glob('theories/**/*.v', recursive=True) + glob('subcomponents/*.v')
+cmd = 'rocq dep -w +default -Q theories/ Stdlib -Q subcomponents subcomponents'
+dependencies : dict[str, list[str]] = {}
+with Popen(cmd.split() + vs, stdout=PIPE, text=True) as proc:
+    for line in proc.stdout:
+        is_vo = lambda s: s.endswith('.vo')
+        (target,), deps = [filter(is_vo, s.split()) for s in line.split(":")]
+        dependencies[target[:-1]] = sorted(d[:-1] for d in deps)
+assert proc.returncode == 0
+
+def is_component(target):
+  return target.startswith('subcomponents/')
+
+@functools.cache
+def comp_requires(a, b):
+    return a == b or any(comp_requires(m, b) for m in compdeps[a])
+
+compdeps = {k : list(filter(is_component, vs)) for k, vs in dependencies.items()}
+component : dict[str, str] = {}
+postorder : dict[str, int] = {}
+def dfs(target, comp, html, dot):
+    if target in component.keys():
+        assert comp_requires(comp, component[target]),\
+               f"{target} (from component {component[target]}) used in {comp}"+\
+               f"but {comp} does not require {component[target]}"
+        return
+    component[target] = comp
+    for dep in compdeps[target]:
+        dfs(dep, dep, html, dot)
+    for dep in dependencies[target]:
+        dfs(dep, comp, html, dot)
+    if html.name == os.devnull and dot.name == os.devnull:
+        return # not printing anything anyway
+    postorder[target] = max(postorder.values(), default=0)+1
+    if is_component(target):
+        minimal = []
+        for dep in sorted(compdeps[target], key=postorder.__getitem__, reverse=True):
+            if not any(comp_requires(e, dep) for e in minimal):
+                minimal.append(dep)
+        p = lambda s: s.split("/")[-1].removesuffix(".v")
+        print ('\n'.join(f"{p(target)} -> {p(dep)};" for dep in minimal), file=dot)
+        name = p(target)
+        print(f'<div class="subcomponent"><dt id="{name}">Subcomponent <a href="#{name}">{name}</a></dt><dd>', file=html)
+        if minimal:
+            deps = [f'<li><a href="#{m}">{m}</a></li>' for m in map(p, minimal)]
+            print(f'depends on <ul class="component-dependencies">{" ".join(deps)}</ul> and ', file=html)
+        print(f'contains <ul class="component-contents">', file=html)
+        compfiles = [k for k,v in component.items() if v == target and k != target]
+        for vfile in sorted(compfiles, key=postorder.__getitem__):
+            m = vfile.removeprefix("theories/").replace("/", ".").removesuffix(".v")
+            print(f'  <li><a href="Stdlib.{m}.html">{m}</a></li>', file=html)
+        print(f'</ul></dd></div>\n', file=html)
+
+html_header = r"""
+<style>
+div.subcomponent {
+  padding-left: 2em;
+  text-indent:-2em;
+  dt {
+    display : inline;
+    margin-right: 0;
+    a { text-decoration: inherit; }
+  }
+  dd {
+    display: inline;
+    margin-left: 0;
+    margin-right: 0;
+    ul {
+      display: inline;
+      padding-left: 0;
+      li {
+        display: inline;
+      }
+    }
+  }
+}
+</style>
+<dl>
+"""
+
+
+dot_header = r"""
+digraph stdlib_deps {
+	rankdir="BT";
+	bgcolor="transparent";
+	node [color="#ff540a",
+		shape=rectangle,
+		style=filled
+		URL="#\N"
+	];
+	edge [color="#260085"];
+"""
+
+assert len(sys.argv) in [1,2,3]
+with open(sys.argv[1] if 1 < len(sys.argv) else os.devnull, 'w') as html,\
+     open(sys.argv[2] if 2 < len(sys.argv) else os.devnull, 'w') as dot:
+  print(html_header, file=html)
+  print(dot_header, file=dot)
+  top = 'subcomponents/all.v'
+  dfs(top, top, html, dot)
+  for target in sorted(dependencies.keys()):
+      if target == top or target == 'theories/All.v':
+          assert component.get(target) == top, target
+          continue
+      assert component.get(target) not in [None, top],\
+              f"{target} does not belong to any component"
+  print("</dl>", file=html)
+  print("}", file=dot)
diff --git a/doc/stdlib/depends.dot b/doc/stdlib/depends.dot
deleted file mode 100644
index fef5b2df79..0000000000
--- a/doc/stdlib/depends.dot
+++ /dev/null
@@ -1,75 +0,0 @@
-# this has been mostly automatically generated by dev/tools/make-depends.sh
-# when editing this, ensure to keep .nix/rocq-overlays/stdlib-subcomponents
-# in sync
-digraph stdlib_deps {
-	node [color="#ff540a",
-		shape=rectangle,
-		style=filled
-		URL="#\N"
-	];
-	bool -> classes;
-	classes -> program;
-	classes -> relations;
-	program -> "corelib-wrapper";
-	program -> logic;
-	strings -> arith;
-	reals -> qarith;
-	reals -> vectors;
-	reals -> "classical-logic";
-	"arith-base" -> structures;
-	zarith -> lia;
-	zmod -> zarith;
-	zmod -> sorting;
-	zmod -> field;
-	qarith -> lqa;
-	positive -> "arith-base";
-	narith -> ring;
-	ring -> lists;
-	ring -> "zarith-base";
-	arith -> ring;
-	structures -> bool;
-	"narith-base" -> positive;
-	lists -> "arith-base";
-	"zarith-base" -> "narith-base";
-	"primitive-int" -> zarith;
-	"primitive-int" -> unicode;
-	lia -> narith;
-	lia -> arith;
-	"fmaps-fsets-msets" -> zarith;
-	"fmaps-fsets-msets" -> "orders-ex";
-	"orders-ex" -> strings;
-	"orders-ex" -> sorting;
-	sets -> "classical-logic";
-	sorting -> lia;
-	sorting -> sets;
-	sorting -> vectors;
-	"primitive-floats" -> "primitive-int";
-	wellfounded -> lists;
-	relations -> "corelib-wrapper";
-	"primitive-string" -> "primitive-int";
-	"primitive-string" -> "orders-ex";
-	vectors -> lists;
-	field -> zarith;
-	lqa -> field;
-	lqa -> "qarith-base";
-	"qarith-base" -> ring;
-	"classical-logic" -> arith;
-	extraction -> "primitive-string";
-	extraction -> "primitive-floats";
-	extraction -> "primitive-array";
-	"primitive-array" -> "primitive-int";
-	streams -> logic;
-	funind -> "arith-base";
-	rtauto -> positive;
-	rtauto -> lists;
-	compat -> zmod;
-	compat -> reals;
-	compat -> "fmaps-fsets-msets";
-	compat -> wellfounded;
-	compat -> "primitive-string";
-	compat -> extraction;
-	compat -> streams;
-	compat -> funind;
-	compat -> rtauto;
-        all -> compat
-}
diff --git a/doc/stdlib/dune b/doc/stdlib/dune
index 4e6e424bc3..1a89cf94af 100644
--- a/doc/stdlib/dune
+++ b/doc/stdlib/dune
@@ -1,14 +1,14 @@
 ; This is an ad-hoc rule to ease the migration, it should be handled
 ; natively by Dune in the future.
 (rule
- (targets index-list.html)
+ (targets index-subcomponents.html depends.dot)
  (deps
-   make-library-index index-list.html.template hidden-files depends.svg
-   (source_tree %{project_root}/theories))
+   %{project_root}/dev/tools/subcomponents.py
+   (source_tree %{project_root}/theories)
+   (source_tree %{project_root}/subcomponents))
  (action
   (chdir %{project_root}
-   ; On windows run will fail
-   (bash "doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files"))))
+   (run env python dev/tools/subcomponents.py doc/stdlib/index-subcomponents.html doc/stdlib/depends.dot))))
 
 (rule
  (targets depends.svg)
@@ -16,9 +16,7 @@
  (action (bash "dot -T svg depends.dot | sed -e 's/width=\".*\"/width=\"100%\"/' > depends.svg")))
 
 (rule
-  (targets (dir html))
-  (alias stdlib-html)
-  (package rocq-stdlib-doc)
+  (targets (dir coqdoc-html))
   (deps
    ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
    (source_tree %{project_root}/theories)
@@ -26,16 +24,35 @@
    (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
    (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
    ; For .glob files, should be gone when Coq Dune is smarter.
+   ; Please update .github/workflows/alpine.yml to still build rocq-stdlib when removing this dependency
    (package rocq-stdlib))
  (action
   (progn
-   (run mkdir -p html)
-   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g --coqlib_url ../corelib -Q %{project_root}/theories Stdlib $(find %{project_root}/theories -name *.v)")
+   (run mkdir -p coqdoc-html)
+   (bash "%{bin:coqdoc} -q -d coqdoc-html --with-header %{header} --with-footer %{footer} --multi-index --html -g --coqlib_url ../corelib -Q %{project_root}/theories Stdlib $(find %{project_root}/theories -name *.v)")
+   )))
+
+(rule
+  (targets (dir html))
+  (alias stdlib-html)
+  (package rocq-stdlib-doc)
+  (deps
+   coqdoc-html
+   index.html
+   index-subcomponents.html
+   depends.svg
+   (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
+   (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html))
+ (action
+  (progn
+   (run cp -ar coqdoc-html html)
    (run mv html/index.html html/genindex.html)
-   (with-stdout-to
-     _index.html
-    (progn (cat %{header}) (cat index-list.html) (cat %{footer})))
-   (run cp depends.svg html/depends.svg)
+   (with-stdout-to _index-subcomponents.html ; dune same-directory restriction
+    (progn (cat %{header}) (echo "<h1>Rocq Standard Library: Internal Component Dependencies</h1>") (cat depends.svg) (cat index-subcomponents.html) (cat %{footer})))
+   (run cp _index-subcomponents.html html/index-subcomponents.html)
+   ; (run cp depends.svg html/depends.svg)
+   (with-stdout-to _index.html ; dune same-directory restriction
+    (progn (cat %{header}) (cat index.html) (cat %{footer})))
    (run cp _index.html html/index.html))))
 
 ; Installable directories are not yet fully supported by Dune.  See
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
deleted file mode 100644
index 125d78c26f..0000000000
--- a/doc/stdlib/hidden-files
+++ /dev/null
@@ -1,165 +0,0 @@
-theories/btauto/Algebra.v
-theories/btauto/Btauto.v
-theories/btauto/Reflect.v
-theories/derive/Derive.v
-theories/extraction/ExtrHaskellBasic.v
-theories/extraction/ExtrHaskellNatInt.v
-theories/extraction/ExtrHaskellNatInteger.v
-theories/extraction/ExtrHaskellNatNum.v
-theories/extraction/ExtrHaskellString.v
-theories/extraction/ExtrHaskellZInt.v
-theories/extraction/ExtrHaskellZInteger.v
-theories/extraction/ExtrHaskellZNum.v
-theories/extraction/ExtrOcamlBasic.v
-theories/extraction/ExtrOcamlChar.v
-theories/extraction/ExtrOCamlInt63.v
-theories/extraction/ExtrOCamlFloats.v
-theories/extraction/ExtrOCamlPArray.v
-theories/extraction/ExtrOcamlIntConv.v
-theories/extraction/ExtrOcamlNatBigInt.v
-theories/extraction/ExtrOcamlNatInt.v
-theories/extraction/ExtrOcamlString.v
-theories/extraction/ExtrOCamlPString.v
-theories/extraction/ExtrOcamlNativeString.v
-theories/extraction/ExtrOcamlZBigInt.v
-theories/extraction/ExtrOcamlZInt.v
-theories/extraction/Extraction.v
-theories/funind/FunInd.v
-theories/funind/Recdef.v
-theories/micromega/Ztac.v
-theories/micromega/DeclConstant.v
-theories/micromega/DeclConstantZ.v
-theories/micromega/Env.v
-theories/micromega/EnvRing.v
-theories/micromega/Fourier.v
-theories/micromega/Fourier_util.v
-theories/micromega/Lia.v
-theories/micromega/Lqa.v
-theories/micromega/Lra.v
-theories/micromega/OrderedRing.v
-theories/micromega/Psatz.v
-theories/micromega/QMicromega.v
-theories/micromega/RMicromega.v
-theories/micromega/Refl.v
-theories/micromega/RingMicromega.v
-theories/micromega/Tauto.v
-theories/micromega/VarMap.v
-theories/micromega/ZArith_hints.v
-theories/micromega/ZCoeff.v
-theories/micromega/ZMicromega.v
-theories/micromega/ZifyInst.v
-theories/micromega/ZifyBool.v
-theories/micromega/ZifyUint63.v
-theories/micromega/ZifySint63.v
-theories/micromega/ZifyNat.v
-theories/micromega/ZifyN.v
-theories/micromega/ZifyComparison.v
-theories/micromega/ZifyClasses.v
-theories/micromega/ZifyPow.v
-theories/micromega/Zify.v
-theories/nsatz/NsatzTactic.v
-theories/omega/OmegaLemmas.v
-theories/omega/PreOmega.v
-theories/rtauto/Bintree.v
-theories/rtauto/Rtauto.v
-theories/setoid_ring/Algebra_syntax.v
-theories/setoid_ring/ArithRing.v
-theories/setoid_ring/BinList.v
-theories/setoid_ring/Cring.v
-theories/setoid_ring/Field.v
-theories/setoid_ring/Field_tac.v
-theories/setoid_ring/Field_theory.v
-theories/setoid_ring/InitialRing.v
-theories/setoid_ring/Integral_domain.v
-theories/setoid_ring/NArithRing.v
-theories/setoid_ring/Ncring.v
-theories/setoid_ring/Ncring_initial.v
-theories/setoid_ring/Ncring_polynom.v
-theories/setoid_ring/Ncring_tac.v
-theories/setoid_ring/RealField.v
-theories/setoid_ring/Ring.v
-theories/setoid_ring/Ring_base.v
-theories/setoid_ring/Ring_polynom.v
-theories/setoid_ring/Ring_tac.v
-theories/setoid_ring/Ring_theory.v
-theories/setoid_ring/Rings_Q.v
-theories/setoid_ring/Rings_R.v
-theories/setoid_ring/Rings_Z.v
-theories/setoid_ring/ZArithRing.v
-theories/ssr/ssrunder.v
-theories/ssr/ssrsetoid.v
-theories/Reals/Cauchy/ConstructiveExtra.v
-theories/Reals/Cauchy/PosExtra.v
-theories/Reals/Cauchy/QExtra.v
-theories/Reals/Nsatz.v
-theories/Numbers/Natural/Binary/NBinary.v
-theories/Numbers/Integer/Binary/ZBinary.v
-theories/Numbers/Integer/NatPairs/ZNatPairs.v
-theories/Numbers/NatInt/NZProperties.v
-theories/Numbers/NatInt/NZDomain.v
-theories/Numbers/Integer/Abstract/ZDivEucl.v
-theories/ZArith/Zeuclid.v
-theories/Arith/Bool_nat.v
-theories/Numbers/Natural/Abstract/NDefOps.v
-theories/Numbers/Natural/Abstract/NIso.v
-theories/Array/ArrayAxioms.v
-theories/Array/PrimArray.v
-theories/BinNums/IntDef.v
-theories/BinNums/NatDef.v
-theories/BinNums/PosDef.v
-theories/Classes/CMorphisms.v
-theories/Classes/CRelationClasses.v
-theories/Classes/Equivalence.v
-theories/Classes/Init.v
-theories/Classes/Morphisms.v
-theories/Classes/Morphisms_Prop.v
-theories/Classes/RelationClasses.v
-theories/Classes/SetoidTactics.v
-theories/Compat/Coq818.v
-theories/Compat/Coq819.v
-theories/Compat/Coq820.v
-theories/Floats/FloatAxioms.v
-theories/Floats/FloatClass.v
-theories/Floats/FloatOps.v
-theories/Floats/PrimFloat.v
-theories/Floats/SpecFloat.v
-theories/Init/Byte.v
-theories/Init/Datatypes.v
-theories/Init/Decimal.v
-theories/Init/Hexadecimal.v
-theories/Init/Logic.v
-theories/Init/Ltac.v
-theories/Init/Nat.v
-theories/Init/Notations.v
-theories/Init/Number.v
-theories/Init/Peano.v
-theories/Init/Prelude.v
-theories/Init/Specif.v
-theories/Init/Sumbool.v
-theories/Init/Tactics.v
-theories/Init/Tauto.v
-theories/Init/Wf.v
-theories/Lists/ListDef.v
-theories/Numbers/BinNums.v
-theories/Numbers/Cyclic/Int63/CarryType.v
-theories/Numbers/Cyclic/Int63/PrimInt63.v
-theories/Numbers/Cyclic/Int63/Sint63Axioms.v
-theories/Numbers/Cyclic/Int63/Uint63Axioms.v
-theories/Program/Basics.v
-theories/Program/Tactics.v
-theories/Program/Utils.v
-theories/Program/Wf.v
-theories/Relations/Relation_Definitions.v
-theories/Setoids/Setoid.v
-theories/Strings/PrimString.v
-theories/Strings/PrimStringAxioms.v
-theories/extraction/ExtrHaskellBasic.v
-theories/extraction/ExtrOcamlBasic.v
-theories/extraction/Extraction.v
-theories/ssr/ssrbool.v
-theories/ssr/ssrclasses.v
-theories/ssr/ssreflect.v
-theories/ssr/ssrfun.v
-theories/ssr/ssrsetoid.v
-theories/ssr/ssrunder.v
-theories/ssrmatching/ssrmatching.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
deleted file mode 100644
index 525fd828f1..0000000000
--- a/doc/stdlib/index-list.html.template
+++ /dev/null
@@ -1,727 +0,0 @@
-
-<h1>The Rocq Standard Library</h1>
-
-<p>This is the index of the Rocq standard library.
-It provides a set of modules directly available
-through the <tt>From Stdlib Require Import</tt> command.</p>
-
-<!-- #include depends.svg -->
-
-<p>The standard library is composed of the following subdirectories:</p>
-
-<dl>
-  <dt> <a name="logic"></a><b>Logic</b>:
-    Logic, dependent equality, extensionality, choice axioms.
-    Look at <a href="#classical-logic">classical-logic</a> for more elaborate results.
-  </dt>
-  <dd>
-    theories/Logic/SetIsType.v
-    theories/Logic/StrictProp.v
-    theories/Logic/Decidable.v
-    theories/Logic/Eqdep_dec.v
-    theories/Logic/EqdepFacts.v
-    theories/Logic/Eqdep.v
-    theories/Logic/JMeq.v
-    theories/Logic/RelationalChoice.v
-    theories/Logic/Berardi.v
-    theories/Logic/Hurkens.v
-    theories/Logic/ProofIrrelevance.v
-    theories/Logic/ProofIrrelevanceFacts.v
-    theories/Logic/ConstructiveEpsilon.v
-    theories/Logic/PropExtensionalityFacts.v
-    theories/Logic/FunctionalExtensionality.v
-    theories/Logic/ExtensionalFunctionRepresentative.v
-    theories/Logic/ExtensionalityFacts.v
-    theories/Logic/WeakFan.v
-    theories/Logic/PropFacts.v
-    theories/Logic/HLevelsBase.v
-    theories/Logic/HLevels.v
-    theories/Logic/Adjointification.v
-  </dd>
-
-  <dt> <a name="program"></a><b>Program</b>:
-    Support for dependently-typed programming
-    Beware that there are also Tactics.v and Wf.v files in Init.
-  </dt>
-  <dd>
-    theories/Program/Subset.v
-    theories/Program/Equality.v
-    theories/Program/Syntax.v
-    theories/Program/WfExtensionality.v
-    theories/Program/Program.v
-    theories/Program/Combinators.v
-  </dd>
-
-  <dt> <a name="relations"></a><b>Relations</b>:
-    Relations (definitions and basic results)
-  </dt>
-  <dd>
-    theories/Relations/Relation_Operators.v
-    theories/Relations/Relations.v
-    theories/Relations/Operators_Properties.v
-  </dd>
-
-  <dt> <a name="classes"></a><b>Classes</b>:
-  </dt>
-  <dd>
-    theories/Classes/Morphisms_Relations.v
-    theories/Classes/CEquivalence.v
-    theories/Classes/SetoidClass.v
-    theories/Classes/RelationPairs.v
-    theories/Classes/DecidableClass.v
-  </dd>
-
-  <dt><a name="bool"></a><b>Bool</b>:
-    Booleans (basic functions and results)
-  </dt>
-  <dd>
-    theories/Bool/Bool.v
-    theories/Bool/BoolEq.v
-    theories/Bool/DecBool.v
-    theories/Bool/IfProp.v
-  </dd>
-
-  <dt> <a name="structures"></a><b>Structures</b>:
-    Basic "algebraic" structures: types with decidable equality and with order.
-    Common instances can be found in <a href="#orders-ex">orders-ex</a>.
-    More developped algebra can be found in the
-    <a href="https://github.com/math-comp/math-comp">mathematical components
-    library</a>.
-  </dt>
-  <dd>
-    theories/Structures/Equalities.v
-    theories/Structures/Orders.v
-    theories/Structures/OrdersTac.v
-    theories/Structures/OrdersFacts.v
-    theories/Structures/GenericMinMax.v
-  </dd>
-
-  <dt> <a name="arith-base"></a><b>Arith-base</b>:
-    Basic Peano Arithmetic.
-    Everything can be loaded with From Stdlib Require Import Arith_base.
-    To enjoy the ring and lia automatic tactic, you additionally need to load
-    arith below, using From Stdlib Require Import Arith Lia.
-  </dt>
-  <dd>
-    theories/Arith/PeanoNat.v
-    theories/Arith/Between.v
-    theories/Arith/Peano_dec.v
-    theories/Arith/Compare_dec.v
-    (theories/Arith/Arith_base.v)
-    theories/Arith/Compare.v
-    theories/Arith/EqNat.v
-    theories/Arith/Euclid.v
-    theories/Arith/Factorial.v
-    theories/Arith/Wf_nat.v
-    theories/Arith/Cantor.v
-    theories/Arith/Zerob.v
-    theories/Numbers/NumPrelude.v
-    theories/Numbers/NatInt/NZAdd.v
-    theories/Numbers/NatInt/NZAddOrder.v
-    theories/Numbers/NatInt/NZAxioms.v
-    theories/Numbers/NatInt/NZBase.v
-    theories/Numbers/NatInt/NZMul.v
-    theories/Numbers/NatInt/NZDiv.v
-    theories/Numbers/NatInt/NZMulOrder.v
-    theories/Numbers/NatInt/NZOrder.v
-    theories/Numbers/NatInt/NZParity.v
-    theories/Numbers/NatInt/NZPow.v
-    theories/Numbers/NatInt/NZSqrt.v
-    theories/Numbers/NatInt/NZLog.v
-    theories/Numbers/NatInt/NZGcd.v
-    theories/Numbers/NatInt/NZBits.v
-    theories/Numbers/Natural/Abstract/NAdd.v
-    theories/Numbers/Natural/Abstract/NAddOrder.v
-    theories/Numbers/Natural/Abstract/NAxioms.v
-    theories/Numbers/Natural/Abstract/NBase.v
-    theories/Numbers/Natural/Abstract/NMulOrder.v
-    theories/Numbers/Natural/Abstract/NOrder.v
-    theories/Numbers/Natural/Abstract/NStrongRec.v
-    theories/Numbers/Natural/Abstract/NSub.v
-    theories/Numbers/Natural/Abstract/NDiv.v
-    theories/Numbers/Natural/Abstract/NDiv0.v
-    theories/Numbers/Natural/Abstract/NMaxMin.v
-    theories/Numbers/Natural/Abstract/NParity.v
-    theories/Numbers/Natural/Abstract/NPow.v
-    theories/Numbers/Natural/Abstract/NSqrt.v
-    theories/Numbers/Natural/Abstract/NLog.v
-    theories/Numbers/Natural/Abstract/NGcd.v
-    theories/Numbers/Natural/Abstract/NLcm.v
-    theories/Numbers/Natural/Abstract/NLcm0.v
-    theories/Numbers/Natural/Abstract/NBits.v
-    theories/Numbers/Natural/Abstract/NProperties.v
-    theories/Classes/SetoidDec.v
-  </dd>
-
-  <dt> <a name="lists"></a><b>Lists</b>:
-    Polymorphic lists
-  </dt>
-  <dd>
-    theories/Lists/List.v
-    theories/Lists/ListDec.v
-    theories/Lists/ListSet.v
-    theories/Lists/ListTactics.v
-    theories/Numbers/NaryFunctions.v
-    theories/Logic/WKL.v
-    theories/Classes/EquivDec.v
-  </dd>
-
-  <dt> <a name="streams"></a><b>Streams</b>:
-    Streams (infinite sequences)
-  </dt>
-  <dd>
-    theories/Streams/Streams.v
-    theories/Streams/StreamMemo.v
-  </dd>
-
-  <dt> <a name="positive"></a><b>PArith</b>:
-    Binary representation of positive integers for effective computation.
-    You may also want narith and zarith below for N and Z
-    built on top of <a href="#positive">positive</a>.
-  </dt>
-  <dd>
-    theories/Numbers/AltBinNotations.v
-    theories/PArith/BinPosDef.v
-    theories/PArith/BinPos.v
-    theories/PArith/Pnat.v
-    theories/PArith/POrderedType.v
-    (theories/PArith/PArith.v)
-  </dd>
-
-  <dt> <a name="narith-base"></a><b>NArith-base</b>:
-    Binary natural numbers.
-    Everything can be loaded with From Stdlib Require Import NArith_base.
-    To enjoy the ring automatic tactic, you need to load
-    <a href="#narith">narith</a> below, using From Stdlib Require Import NArith.
-  </dt>
-  <dd>
-    theories/NArith/BinNatDef.v
-    theories/NArith/BinNat.v
-    theories/NArith/Nnat.v
-    theories/NArith/Ndec.v
-    theories/NArith/Ndiv_def.v
-    theories/NArith/Ngcd_def.v
-    theories/NArith/Nsqrt_def.v
-    (theories/NArith/NArith_base.v)
-  </dd>
-
-  <dt> <a name="narith"></a><b>NArith</b>:
-    Binary natural numbers
-  </dt>
-  <dd>
-    (theories/NArith/NArith.v)
-  </dd>
-
-  <dt> <a name="zarith-base"></a><b>ZArith-base</b>:
-    Basic binary integers
-  </dt>
-  <dd>
-    theories/Numbers/Integer/Abstract/ZAdd.v
-    theories/Numbers/Integer/Abstract/ZAddOrder.v
-    theories/Numbers/Integer/Abstract/ZAxioms.v
-    theories/Numbers/Integer/Abstract/ZBase.v
-    theories/Numbers/Integer/Abstract/ZLt.v
-    theories/Numbers/Integer/Abstract/ZMul.v
-    theories/Numbers/Integer/Abstract/ZMulOrder.v
-    theories/Numbers/Integer/Abstract/ZSgnAbs.v
-    theories/Numbers/Integer/Abstract/ZMaxMin.v
-    theories/Numbers/Integer/Abstract/ZParity.v
-    theories/Numbers/Integer/Abstract/ZPow.v
-    theories/Numbers/Integer/Abstract/ZGcd.v
-    theories/Numbers/Integer/Abstract/ZLcm.v
-    theories/Numbers/Integer/Abstract/ZBits.v
-    theories/Numbers/Integer/Abstract/ZProperties.v
-    theories/Numbers/Integer/Abstract/ZDivFloor.v
-    theories/Numbers/Integer/Abstract/ZDivTrunc.v
-    theories/ZArith/BinIntDef.v
-    theories/ZArith/BinInt.v
-    theories/ZArith/Zorder.v
-    theories/ZArith/Zcompare.v
-    theories/ZArith/Znat.v
-    theories/ZArith/Zmin.v
-    theories/ZArith/Zmax.v
-    theories/ZArith/Zminmax.v
-    theories/ZArith/Zabs.v
-    theories/ZArith/Zeven.v
-    theories/ZArith/auxiliary.v
-    theories/ZArith/ZArith_dec.v
-    theories/ZArith/Zbool.v
-    theories/ZArith/Zmisc.v
-    theories/ZArith/Wf_Z.v
-    theories/ZArith/Zhints.v
-    (theories/ZArith/ZArith_base.v)
-    theories/ZArith/Zpow_alt.v
-    theories/ZArith/Int.v
-  </dd>
-
-  <dt> <a name="ring"></a><b>Ring</b>:
-    Ring tactic.
-  </dt>
-  <dd>
-    theories/ZArith/Zcomplements.v
-    theories/ZArith/Zpow_def.v
-    theories/ZArith/Zdiv.v
-    theories/ZArith/Znumtheory.v
-    theories/ZArith/Zdivisibility.v
-    theories/ZArith/Zcong.v
-  </dd>
-
-  <dt> <a name="arith"></a><b>Arith</b>:
-    Basic Peano arithmetic
-  </dt>
-  <dd>
-    (theories/Arith/Arith.v)
-  </dd>
-
-  <dt> <a name="zarith"></a><b>ZArith</b>:
-    Binary encoding of integers.
-    This binary encoding was initially developped to enable effective
-    computations, compared to the unary encoding of nat. Proofs were then added
-    making the types usable for mathematical proofs, although this was not
-    the initial intent. If even-more efficient computations are needed, look
-    at the <a href="#primitive-int">primitive-int</a> package below for 63 bits machine arithmetic
-    or the coq-bignums package for arbitrary precision machine arithmetic.
-    Everything can be imported with From Stdlib Require Import ZArith.
-    Also contains the migromega tactic that can be loaded with
-    From Stdlib Require Import Lia.
-  </dt>
-  <dd>
-    theories/ZArith/Zpower.v
-    theories/ZArith/Zquot.v
-    (theories/ZArith/ZArith.v)
-    theories/ZArith/Zgcd_alt.v
-    theories/ZArith/Zwf.v
-    theories/ZArith/Zpow_facts.v
-    theories/ZArith/Zdiv_facts.v
-    theories/ZArith/Zbitwise.v
-    theories/ZArith/ZModOffset.v
-    theories/ZArith/ZNsatz.v
-    theories/Numbers/DecimalFacts.v
-    theories/Numbers/DecimalNat.v
-    theories/Numbers/DecimalPos.v
-    theories/Numbers/DecimalN.v
-    theories/Numbers/DecimalZ.v
-    theories/Numbers/HexadecimalFacts.v
-    theories/Numbers/HexadecimalNat.v
-    theories/Numbers/HexadecimalPos.v
-    theories/Numbers/HexadecimalN.v
-    theories/Numbers/HexadecimalZ.v
-  </dd>
-
-  <dt> <a name="zmod"></a><b>Zmod and Zstar</b>:
-    Modular arithmetic -- integers modulo another integer -- including machine
-    words (bitvectors) and the multiplicative group of integers modulo another
-    integer.
-  </dt>
-  <dd>
-    theories/Zmod/Zmod.v
-    theories/Zmod/Bits.v
-    theories/Zmod/Zstar.v
-    (theories/Zmod/ZmodDef.v)
-    (theories/Zmod/ZstarDef.v)
-    (theories/Zmod/ZmodBase.v)
-    (theories/Zmod/ZstarBase.v)
-    (theories/Zmod/ZmodInv.v)
-  </dd>
-
-  <dt> <a name="unicode"></a><b>Unicode</b>:
-    Unicode-based alternative notations
-  </dt>
-  <dd>
-    theories/Unicode/Utf8_core.v
-    theories/Unicode/Utf8.v
-  </dd>
-
-  <dt> <a name="primitive-int"></a><b>Primitive Integers</b>:
-    Interface for hardware integers (63 rather than 64 bits due to OCaml
-    garbage collector). This enables very efficient arithmetic, for developing
-    tactics for proofs by reflection for instance.
-  </dt>
-  <dd>
-    theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
-    theories/Numbers/Cyclic/Abstract/NZCyclic.v
-    theories/Numbers/Cyclic/Abstract/DoubleType.v
-    theories/Numbers/Cyclic/Int63/Cyclic63.v
-    theories/Numbers/Cyclic/Int63/Uint63.v
-    theories/Numbers/Cyclic/Int63/Sint63.v
-    theories/Numbers/Cyclic/Int63/Ring63.v
-  </dd>
-
-  <dt> <a name="primitive-floats"></a><b>Floats</b>:
-    Efficient machine floating-point arithmetic
-    Interface to hardware floating-point arithmetic for efficient computations.
-    This offers a basic model of floating-point arithmetic but is not very
-    usable alone. Look at the coq-flocq package for an actual model of
-    floating-point arithmetic, including links to Stdlib <a href="#reals">reals</a> and the current
-    Floats.
-  </dt>
-  <dd>
-    theories/Floats/FloatLemmas.v
-    (theories/Floats/Floats.v)
-  </dd>
-
-  <dt> <a name="primitive-array"></a><b>Primitive Arrays</b>:
-    Persistent native arrays, enabling efficient computations with arrays.
-  </dt>
-  <dd>
-    theories/Array/PArray.v
-  </dd>
-
-  <dt> <a name="vectors"></a><b>Vectors</b>:
-    Dependent datastructures storing their length.
-    This is known to be technically difficult to use. It is often much better
-    to use a dependent pair with a list and a proof about its length,
-    as provided by the tuple type in package coq-mathcomp-ssreflect,
-    allowing almost transparent mixing with lists.
-  </dt>
-  <dd>
-    theories/Vectors/Fin.v
-    theories/Vectors/VectorDef.v
-    theories/Vectors/VectorSpec.v
-    theories/Vectors/VectorEq.v
-    (theories/Vectors/Vector.v)
-    theories/Vectors/FinFun.v
-    theories/Vectors/Bvector.v
-  </dd>
-
-  <dt> <a name="strings"></a><b>Strings</b>
-    Implementation of string as list of ASCII characters
-    Beware that there is also a Byte.v file in Init.
-  </dt>
-  <dd>
-    theories/Strings/Byte.v
-    theories/Strings/Ascii.v
-    theories/Strings/String.v
-    theories/Strings/BinaryString.v
-    theories/Strings/HexString.v
-    theories/Strings/OctalString.v
-    theories/Numbers/DecimalString.v
-    theories/Numbers/HexadecimalString.v
-  </dd>
-
-  <dt> <a name="classical-logic"></a><b>Classical Logic</b>:
-    Classical logic, dependent equality, extensionality, choice axioms
-  </dt>
-  <dd>
-    theories/Logic/Classical_Pred_Type.v
-    theories/Logic/Classical_Prop.v
-    (theories/Logic/Classical.v)
-    theories/Logic/ClassicalFacts.v
-    theories/Logic/ChoiceFacts.v
-    theories/Logic/ClassicalChoice.v
-    theories/Logic/ClassicalDescription.v
-    theories/Logic/ClassicalEpsilon.v
-    theories/Logic/ClassicalUniqueChoice.v
-    theories/Logic/SetoidChoice.v
-    theories/Logic/Diaconescu.v
-    theories/Logic/Description.v
-    theories/Logic/Epsilon.v
-    theories/Logic/IndefiniteDescription.v
-    theories/Logic/PropExtensionality.v
-  </dd>
-
-  <dt> <a name="sets"></a><b>Sets</b>:
-    Classical sets. This is known to be outdated. More modern alternatives
-    can be found in coq-mathcomp-ssreflect (for finite sets)
-    and coq-mathcomp-classical (for classical sets) or coq-stdpp.
-  </dt>
-  <dd>
-    theories/Sets/Classical_sets.v
-    theories/Sets/Constructive_sets.v
-    theories/Sets/Cpo.v
-    theories/Sets/Ensembles.v
-    theories/Sets/Finite_sets_facts.v
-    theories/Sets/Finite_sets.v
-    theories/Sets/Image.v
-    theories/Sets/Infinite_sets.v
-    theories/Sets/Integers.v
-    theories/Sets/Multiset.v
-    theories/Sets/Partial_Order.v
-    theories/Sets/Permut.v
-    theories/Sets/Powerset_Classical_facts.v
-    theories/Sets/Powerset_facts.v
-    theories/Sets/Powerset.v
-    theories/Sets/Relations_1_facts.v
-    theories/Sets/Relations_1.v
-    theories/Sets/Relations_2_facts.v
-    theories/Sets/Relations_2.v
-    theories/Sets/Relations_3_facts.v
-    theories/Sets/Relations_3.v
-    theories/Sets/Uniset.v
-  </dd>
-
-  <dt> <a name="sorting"></a><b>Sorting</b>:
-    Axiomatizations of sorts
-  </dt>
-  <dd>
-    theories/Sorting/SetoidList.v
-    theories/Sorting/SetoidPermutation.v
-    theories/Sorting/Heap.v
-    theories/Sorting/Permutation.v
-    theories/Sorting/Sorting.v
-    theories/Sorting/PermutEq.v
-    theories/Sorting/PermutSetoid.v
-    theories/Sorting/Mergesort.v
-    theories/Sorting/Sorted.v
-    theories/Sorting/CPermutation.v
-  </dd>
-
-  <dt> <a name="orders-ex"></a><b>Structure Instances</b>:
-    Instances of order structures from <a href="#structures">Structures</a> above.
-    DecidableType* and OrderedType* are there only for compatibility.
-  </dt>
-  <dd>
-    theories/Structures/EqualitiesFacts.v
-    theories/Structures/OrdersAlt.v
-    theories/Structures/OrdersEx.v
-    theories/Structures/OrdersLists.v
-    theories/Structures/DecidableType.v
-    theories/Structures/DecidableTypeEx.v
-    theories/Structures/OrderedType.v
-    theories/Structures/OrderedTypeAlt.v
-    theories/Structures/OrderedTypeEx.v
-    theories/Structures/BoolOrder.v
-  </dd>
-
-  <dt> <a name="primitive-string"></a><b>Primitive Strings</b>
-    Native string type
-  </dt>
-  <dd>
-    theories/Strings/PString.v
-  </dd>
-
-  <dt> <a name="qarith-base"></a><b>QArith-base</b>:
-    Basic binary rational numbers.
-    Look at <a href="#qarith">qarith</a> below for more functionalities with the field
-    and Lqa tactics.
-  </dt>
-  <dd>
-    theories/QArith/QArith_base.v
-    theories/QArith/Qreduction.v
-    theories/QArith/QOrderedType.v
-    theories/QArith/Qminmax.v
-  </dd>
-
-  <dt> <a name="field"></a><b>Field</b>:
-    Field tactic.
-  </dt>
-  <dd>
-    theories/QArith/Qpower.v
-    theories/QArith/Qring.v
-    theories/QArith/Qfield.v
-    theories/QArith/Qcanon.v
-    theories/QArith/Qround.v
-  </dd>
-
-  <dt> <a name="qarith"></a><b>QArith</b>:
-    Binary rational numbers, made on top of <a href="#zarith">zarith</a>.
-    Those enable effective computations in arbitrary precision exact rational
-    arithmetic. Those rationals are known to be difficult to use for
-    mathematical proofs because there is no canonical representation
-    (2/3 and 4/6 are not equal for instance). For even more efficient
-    computation, look at the coq-bignums package which uses machine integers.
-    For mathematical proofs, the rat type of the coq-mathcomp-algebra package
-    are much more comfortable, although they don't enjoy efficient computation
-    (coq-coqeal offers a refinement with coq-bignums that enables to enjoy
-    both aspects).
-  </dt>
-  <dd>
-    theories/QArith/Qabs.v
-    (theories/QArith/QArith.v)
-    theories/QArith/Qcabs.v
-    theories/QArith/QNsatz.v
-    theories/Numbers/DecimalQ.v
-    theories/Numbers/HexadecimalQ.v
-  </dd>
-
-  <dt> <a name="reals"></a><b>Reals</b>:
-    Formalization of real numbers.
-    Most of it can be loaded with From Stdlib Require Import Reals.
-    Also contains the micromega tactics, loadable with
-    From Stdlib Require Import Lra. and From Stdlib Require Import Psatz.
-  </dt>
-  <dd>
-    <dl>
-  <dt> <b>Classical Reals</b>:
-    Real numbers with excluded middle, total order and least upper bounds
-  </dt>
-  <dd>
-    theories/Reals/Rdefinitions.v
-    theories/Reals/ClassicalDedekindReals.v
-    theories/Reals/ClassicalConstructiveReals.v
-    theories/Reals/Raxioms.v
-    theories/Reals/RIneq.v
-    theories/Reals/DiscrR.v
-    theories/Reals/ROrderedType.v
-    theories/Reals/Rminmax.v
-    (theories/Reals/Rbase.v)
-    theories/Reals/RList.v
-    theories/Reals/Ranalysis.v
-    theories/Reals/Rbasic_fun.v
-    theories/Reals/Rderiv.v
-    theories/Reals/Rfunctions.v
-    theories/Reals/Zfloor.v
-    theories/Reals/Rgeom.v
-    theories/Reals/R_Ifp.v
-    theories/Reals/Rlimit.v
-    theories/Reals/Rseries.v
-    theories/Reals/Rsigma.v
-    theories/Reals/R_sqr.v
-    theories/Reals/Rtrigo_fun.v
-    theories/Reals/Rtrigo1.v
-    theories/Reals/Rtrigo.v
-    theories/Reals/Rtrigo_facts.v
-    theories/Reals/Ratan.v
-    theories/Reals/Machin.v
-    theories/Reals/SplitAbsolu.v
-    theories/Reals/SplitRmult.v
-    theories/Reals/Alembert.v
-    theories/Reals/AltSeries.v
-    theories/Reals/ArithProp.v
-    theories/Reals/Binomial.v
-    theories/Reals/Cauchy_prod.v
-    theories/Reals/Cos_plus.v
-    theories/Reals/Cos_rel.v
-    theories/Reals/Exp_prop.v
-    theories/Reals/Integration.v
-    theories/Reals/MVT.v
-    theories/Reals/NewtonInt.v
-    theories/Reals/PSeries_reg.v
-    theories/Reals/PartSum.v
-    theories/Reals/R_sqrt.v
-    theories/Reals/Ranalysis1.v
-    theories/Reals/Ranalysis2.v
-    theories/Reals/Ranalysis3.v
-    theories/Reals/Ranalysis4.v
-    theories/Reals/Ranalysis5.v
-    theories/Reals/Ranalysis_reg.v
-    theories/Reals/Rcomplete.v
-    theories/Reals/RiemannInt.v
-    theories/Reals/RiemannInt_SF.v
-    theories/Reals/Rpow_def.v
-    theories/Reals/Rpower.v
-    theories/Reals/Rprod.v
-    theories/Reals/Rsqrt_def.v
-    theories/Reals/Rtopology.v
-    theories/Reals/Rtrigo_alt.v
-    theories/Reals/Rtrigo_calc.v
-    theories/Reals/Rtrigo_def.v
-    theories/Reals/Rtrigo_reg.v
-    theories/Reals/SeqProp.v
-    theories/Reals/SeqSeries.v
-    theories/Reals/Sqrt_reg.v
-    theories/Reals/Rlogic.v
-    theories/Reals/RNsatz.v
-    theories/Reals/Rregisternames.v
-    (theories/Reals/Reals.v)
-    theories/Reals/Runcountable.v
-  </dd>
-  <dt> <b>Abstract Constructive Reals</b>:
-    Interface of constructive reals, proof of equivalence of all implementations. EXPERIMENTAL 
-  </dt>
-  <dd>
-    theories/Reals/Abstract/ConstructiveReals.v
-    theories/Reals/Abstract/ConstructiveRealsMorphisms.v
-    theories/Reals/Abstract/ConstructiveLUB.v
-    theories/Reals/Abstract/ConstructiveAbs.v
-    theories/Reals/Abstract/ConstructiveLimits.v
-    theories/Reals/Abstract/ConstructiveMinMax.v
-    theories/Reals/Abstract/ConstructivePower.v
-    theories/Reals/Abstract/ConstructiveSum.v
-  </dd>
-  <dt> <b>Constructive Cauchy Reals</b>:
-    Cauchy sequences of rational numbers, implementation of the interface. EXPERIMENTAL
-  </dt>
-  <dd>
-    theories/Reals/Cauchy/ConstructiveRcomplete.v
-    theories/Reals/Cauchy/ConstructiveCauchyReals.v
-    theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
-    theories/Reals/Cauchy/ConstructiveCauchyAbs.v
-    theories/Reals/Qreals.v
-    theories/Numbers/DecimalR.v
-    theories/Numbers/HexadecimalR.v
-  </dd>
-
-  </dl>
-  </dd>
-
-  <dt> <a name="fmaps-fsets-msets"></a><b>MSets</b>:
-    Modular implementation of finite sets using lists or
-    efficient trees. This is a modernization of FSets.
-  </dt>
-  <dd>
-    theories/MSets/MSetInterface.v
-    theories/MSets/MSetFacts.v
-    theories/MSets/MSetDecide.v
-    theories/MSets/MSetProperties.v
-    theories/MSets/MSetEqProperties.v
-    theories/MSets/MSetWeakList.v
-    theories/MSets/MSetList.v
-    theories/MSets/MSetGenTree.v
-    theories/MSets/MSetAVL.v
-    theories/MSets/MSetRBT.v
-    theories/MSets/MSetPositive.v
-    theories/MSets/MSetToFiniteSet.v
-    (theories/MSets/MSets.v)
-  </dd>
-
-  <dt> <b>FSets</b>:
-    Modular implementation of finite sets/maps using lists or
-    efficient trees. For sets, please consider the more
-    modern MSets.
-  </dt>
-  <dd>
-    theories/FSets/FSetInterface.v
-    theories/FSets/FSetBridge.v
-    theories/FSets/FSetFacts.v
-    theories/FSets/FSetDecide.v
-    theories/FSets/FSetProperties.v
-    theories/FSets/FSetEqProperties.v
-    theories/FSets/FSetList.v
-    theories/FSets/FSetWeakList.v
-    theories/FSets/FSetCompat.v
-    theories/FSets/FSetAVL.v
-    theories/FSets/FSetPositive.v
-    (theories/FSets/FSets.v)
-    theories/FSets/FSetToFiniteSet.v
-    theories/FSets/FMapInterface.v
-    theories/FSets/FMapWeakList.v
-    theories/FSets/FMapList.v
-    theories/FSets/FMapPositive.v
-    theories/FSets/FMapFacts.v
-    (theories/FSets/FMaps.v)
-    theories/FSets/FMapAVL.v
-    theories/FSets/FMapFullAVL.v
-  </dd>
-
-  <dt> <a name="wellfounded"></a><b>Wellfounded</b>:
-    Well-founded Relations
-  </dt>
-  <dd>
-    theories/Wellfounded/Disjoint_Union.v
-    theories/Wellfounded/Inclusion.v
-    theories/Wellfounded/Inverse_Image.v
-    theories/Wellfounded/Lexicographic_Exponentiation.v
-    theories/Wellfounded/Lexicographic_Product.v
-    theories/Wellfounded/List_Extension.v
-    theories/Wellfounded/Transitive_Closure.v
-    theories/Wellfounded/Union.v
-    theories/Wellfounded/Wellfounded.v
-    theories/Wellfounded/Well_Ordering.v
-  </dd>
-
-  <dt> <a name="compat"></a><b>Compat</b>:
-    Compatibility wrappers for previous versions of Stdlib
-  </dt>
-  <dd>
-    theories/Compat/AdmitAxiom.v
-    theories/Compat/Stdlib818.v
-  </dd>
-
-  <dt> <a name="all"></a><b>All</b>:
-    Require the whole Stdlib
-  </dt>
-  <dd>
-    (theories/All/All.v)
-  </dd>
-</dl>
diff --git a/doc/stdlib/index.html b/doc/stdlib/index.html
new file mode 100644
index 0000000000..9562958f78
--- /dev/null
+++ b/doc/stdlib/index.html
@@ -0,0 +1,142 @@
+<style>
+dl { div {
+  padding-left: 2em;
+  text-indent:-2em;
+  dt {
+    display : inline;
+    margin-right: 0;
+    a { text-decoration: inherit; }
+  }
+  dd {
+    display: inline;
+    margin-left: 0;
+    margin-right: 0;
+    ul {
+      display: inline;
+      padding-left: 0;
+      li {
+        display: inline;
+      }
+    }
+  }
+}}
+</style>
+
+<h1>The Rocq Standard Library</h1>
+
+<p>These modules are available through the <code>From Stdlib Require Import</code> command.</p>
+
+<p>This table of components covers top-level modules intended for direct use.
+For an exhaustive listing of standard-library modules (public and internal) as well as the internal dependencies between them, see the <a href="index-subcomponents.html">subcomponent index</a>.
+There is also an <a href="genindex.html">alphabetical index</a> of all modules and objects.
+
+<p>To find specific lemmas and defintions in the standard library, do <code>From Stdlib Require All.</code> (no <code>Import</code>!) and use the <code><a href="../refman/proof-engine/vernacular-commands.html#coq:cmd.Search">Search</a></code> command, for example <code>Search (_ * (_ + _)).</code></p>
+
+<h2>Concrete Computable Objects</h2>
+
+<dl>
+  <div id="Bool"><dt><a href="Stdlib.Bool.Bool.html">Bool</a></dt>
+    <dd>Booleans <code><a href="../corelib/Corelib.Init.Datatypes.html#bool">bool</a></code> (<code>true</code> and <code>false</code>), boolean operators, and their properties.</dd>
+  </div>
+  <div id="Byte"><dt><a href="Stdlib.Strings.Byte.html">Byte</a></dt>
+    <dd>A variant type with 256 cases.</dd>
+  </div>
+  <div id="PeanoNat"><dt><a href="Stdlib.Arith.PeanoNat.html">PeanoNat</a></dt>
+    <dd>Unary natural numbers <code><a href="../corelib/Corelib.Init.Datatypes.html#nat">nat</a></code>. The first-principles construction in this module is intended for learning, use for structural recursion, and for type indices in advanced dependently typed programming. For code that treats natural numbers opaquely, consider <a href="#NArith">NArith</a>. </dd>
+  </div>
+  <div id="List"><dt><a href="Stdlib.Lists.List.html">List</a></dt>
+    <dd>Lists of any element type (e.g. <code><a href="../corelib/Corelib.Init.Datatypes.html#list">list</a> nat</code>).</dd>
+  </div>
+  <div id="NArith"><dt><a href="Stdlib.NArith.NArith.html">NArith</a></dt>
+    <dd>Natural numbers <code><a href="../corelib/Corelib.Numbers.BinNums.html#N">N</a></code>. For Peano induction, use <code><a href="Stdlib.NArith.BinNat.html#N.peano_ind">N.peano_ind</a></code>.</dd>
+  </div>
+  <div id="ZArith"><dt><a href="Stdlib.ZArith.ZArith.html">ZArith</a></dt>
+    <dd>Integers <code><a href="../corelib/Corelib.Numbers.BinNums.html#Z">Z</a></code>. Induction: <code><a href="Stdlib.ZArith.BinInt.html#Z.peano_ind">Z.peano_ind</a></code>, <code>Z.order_induction_0</code> or, for non-negative, <code><a href="Stdlib.ZArith.Wf_Z.html#natlike_ind">Wf_Z.natlike_ind</a></code>.</dd>
+  </div>
+  <div id="Zmod"><dt><a href="Stdlib.Zmod.Zmod.html">Zmod</a></dt>
+    <dd>Integers modulo another integer (<code><a href="Stdlib.Zmod.ZmodDef.html#Zmod.Zmod">Zmod</a> m</code>).</dd>
+  </div>
+  <div id="Bits"><dt><a href="Stdlib.Zmod.Bits.html">Bits</a></dt>
+    <dd>Machine integers, machine words, or bitvectors (<code><a href="Stdlib.Zmod.ZmodDef.html#bits">bits</a> n</code>).</dd>
+  </div>
+  <div id="Zstar"><dt><a href="Stdlib.Zmod.Zstar.html">Zstar</a></dt>
+    <dd>Multiplicative group of coprime integers modulo another integer (<code><a href="Stdlib.Zmod.ZstarDef.html#Zstar.Zstar">Zstar</a> m</code>).</dd>
+  </div>
+  <div id="QArith"><dt><a href="Stdlib.QArith.QArith.html">QArith</a></dt>
+    <dd>Rational numbers with canonical and non-canonical representations (<code><a href="https://rocq-prover.org/doc/master/stdlib/Stdlib.QArith.Qcanon.html#Qc">Qc</a></code> and <code><a href="https://rocq-prover.org/doc/master/stdlib/Stdlib.QArith.QArith_base.html#Q">Q</a></code>). Also consider <code>rat</code> from <a href="https://math-comp.github.io/">math-comp</a> or <code>bigQ</code> from <a href="https://github.com/rocq-community/bignums">coq-bignums</a>.</dd>
+  </div>
+  <div id="SpecFloat"><dt><a href="Stdlib.Floats.SpecFloat.html">SpecFloat</a></dt>
+    <dd>Floating-point numbers <code><a href="../corelib/Corelib.Floats.SpecFloat.html#spec_float">spec_float</a></code>, defined following the fully specified subset of IEEE-754 (without NaN payloads). Continued in <a href="http://flocq.gforge.inria.fr/">flocq</a>.</dd>
+  </div>
+</dl>
+
+<h2>Programming Aides</h2>
+<dl>
+  <div id="unicode"><dt><a href="Stdlib.Unicode.Utf8.html">Utf8</a></dt>
+    <dd>notations for quantifiers and operators.</dd>
+  </div>
+  <div id="Wf"><dt><a href="Stdlib.Init.Wf.html">Wf</a></dt>
+    <dd>well-founded recursion (<code><a href="../corelib/Corelib.Init.Wf.html#Fix">Fix</a></code>) for non-structural recursion based on a termination proof.</dd>
+  </div>
+  <div id="Wellfounded"><dt><a href="Stdlib.Wellfounded.Wellfounded.html">Wellfounded</a></dt>
+    <dd>Relations without infinite descending chains for termination proofs.</dd>
+  </div>
+  <div id="Program"><dt><a href="Stdlib.Program.Program.html">Program</a></dt>
+    <dd>More intensive elaboration; documented in the Rocq Prover manual: <a href="https://rocq-prover.org/doc/master/refman/addendum/program.html">Program</a>. Also consider <a href="https://mattam82.github.io/Coq-Equations/">rocq-equations</a>.
+  </div>
+</dl>
+
+<h2>Decision Procedures</h2>
+
+<p>Documented in the Rocq Prover manual: <a href="../refman/proofs/automatic-tactics/index.html">Automatic Solvers</a>.</p>
+
+<h2>Real Numbers</h2>
+<dl>
+  <div id="Reals"><dt><a href="Stdlib.Reals.Reals.html">Reals</a></dt>
+    <dd>Classical real numbers <code><a href="Stdlib.Reals.Rdefinitions.html#RbaseSymbolsImpl.R">R</a></code> with excluded middle, total order and least upper bounds.</dd>
+  </div>
+  <div id="ConstructiveReals"><dt><a href="Stdlib.Reals.Abstract.ConstructiveReals.html">Reals</a></dt>
+    <dd>Axiomatization and uniqeness of constructive real numbers.</dd>
+  </div>
+  <div id="Cauchy.ConstructiveRcomplete"><dt><a href="Stdlib.Reals.Cauchy.ConstructiveRcomplete.html">Cauchy.ConstructiveRcomplete</a></dt>
+    <dd>Construction and completeness of Cauchy real numbers.</dd>
+  </div>
+</dl>
+
+<h2>Advanced Dependendly Typed Programming</h2>
+
+<dl>
+  <div id="EqDep_dec"><dt><a href="Stdlib.Logic.Eqdep_dec.html">EqDep_dec</a></dt><dd>Uniqueness of proofs of decidable equalities.</dd></div>
+  <div id="Vector"><dt><a href="Stdlib.Vector.Vector.html">Vector</a></dt>
+    <dd>Lists with length-dependent type, constructed as an inductive type indexed by a <code>nat</code> (the length). This construction is uniquely suitable for nesting with other inductive types, but direct proofs about it require skilled use of dependent pattern matching with an <code>in</code> clause. Indirect reasoning about vectors converted to lists is often preferred. If nesting is not needed, consider using <code>list</code>, potentially paired with a proof about its length.</dd>
+  </div>
+  <div id="Fin"><dt><a href="Stdlib.Vector.Fin.html">Fin</a></dt>
+    <dd>Bounded natural numbers, constructed as an inductive type indexed by a <code>nat</code> (the strict upper bound). This construction matches the index space of <a href="#Vector">Vector</a>, but again direct proofs about it require skilled use of dependent pattern matching with an <code>in</code> clause. Further, <code>Fin.t n</code> is inhabited only if <code>n</code> is nonzero, so a natural number cannot be a always converted to <code>Fin.t</code> (unlike <code>Zmod 0</code>, which is isomorphic to <code>Z</code>).</dd>
+  </div>
+</dl>
+
+<h2>Study of Rocq's Logic</h2>
+
+The standard library contains substantial study of near-paradoxes and edge cases in Rocq's logic. See the <a href="index-subcomponents.html#logic">logic</a> and <a href="index-subcomponents.html#classical_logic">classical-logic</a> subcomponents. However, if looking at the included <a href="index-subcomponents.html#sets">sets</a> library, also consider <a href="https://github.com/math-comp/analysis/tree/master/classical">math-comp/analysis/classical</a>.
+
+<h2>Axiomatized OCaml Primitives</h2>
+
+<p>Rocq Prover documentation: <a href="../refman/language/core/primitive.html">Primitive Objects</a>.</p>
+
+<dl>
+  <div id="Uint63"><dt><a href="Stdlib.Numbers.Cyclic.Int63.Uint63.html">Uint63</a></dt>
+    <dd>OCaml 63-bit unsigned integers and axioms relating them to <code><a href="../corelib/Corelib.Numbers.BinNums.html#Z">Z</a></code>.</dd>
+  </div>
+  <div id="Sint63"><dt><a href="Stdlib.Numbers.Cyclic.Int63.Uint63.html">Sint63</a></dt>
+    <dd>OCaml 63-bit signed integers and axioms relating them to <code><a href="../corelib/Corelib.Numbers.BinNums.html#Z">Z</a></code>.</dd>
+  </div>
+  <div id="Floats"><dt><a href="Stdlib.Floats.Floats.html">Floats</a></dt>
+    <dd>Hardware floating-point arithmetic and axioms relating them to <a href="Stdlib.Floats.SpecFloat.html">SpecFloat</a>.<dd>
+  </div>
+  <div id="PArray"><dt><a href="Stdlib.Array.PArray.html">PArray</a></dt>
+    <dd>Persistent arrays implemented in OCaml using internal mutability.</dd>
+  </div>
+  <div id="PString"><dt><a href="Stdlib.Strings.PString.html">PString</a></dt>
+    <dd></dd>
+  </div>
+</dl>
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
deleted file mode 100755
index b7361819d9..0000000000
--- a/doc/stdlib/make-library-index
+++ /dev/null
@@ -1,52 +0,0 @@
-#!/usr/bin/env bash
-
-# Instantiate links to library files in index template
-
-set -e
-
-FILE=$1
-HIDDEN=$2
-tmp=$(mktemp)
-tmp2=$(mktemp)
-
-sed -e '/#include depends.svg/r doc/stdlib/depends.svg' "$FILE.template" > "$tmp"
-echo -n "Building file index-list.prehtml... "
-
-LIBDIRS=$(find theories/* -type d ! -name .coq-native)
-
-for k in $LIBDIRS; do
-    BASE_PREFIX="Stdlib."
-    d=$(basename "$k")
-    for j in "$k"/*.v; do
-        if ! [ -e "$j" ]; then break; fi
-        b=$(basename "$j" .v)
-
-        a=0; grep -q "$k/$b.v" "$tmp" || a=$?
-        h=0; grep -q "$k/$b.v" "$HIDDEN" || h=$?
-        if [ $a = 0 ]; then
-            if [ $h = 0 ]; then
-                echo "Error: $FILE and $HIDDEN both mention $k/$b.v" >&2
-                exit 1
-            else
-                p=$(echo "$k" | sed 's:^[^/]*/::' | sed 's:/:.:g')
-                sed -e "s:$k/$b.v:<a href=\"$BASE_PREFIX$p.$b.html\">$b</a>:g" "$tmp" > "$tmp2"
-                mv -f "$tmp2" "$tmp"
-            fi
-        else
-            if [ $h = 0 ]; then
-                # Skipping file from the index
-                :
-            else
-                echo "Error: none of $FILE and $HIDDEN mention $k/$b.v" >&2
-                exit 1
-            fi
-
-        fi
-    done
-    sed -e "s/#$d#//" "$tmp" > "$tmp2"
-    mv -f "$tmp2" "$tmp"
-done
-
-if a=$(grep theories "$tmp"); then echo Error: extra files: >&2; echo "$a" >&2; exit 1; fi
-mv "$tmp" "$FILE"
-echo Done
diff --git a/subcomponents/all.v b/subcomponents/all.v
new file mode 100644
index 0000000000..9245399f0a
--- /dev/null
+++ b/subcomponents/all.v
@@ -0,0 +1,2 @@
+From subcomponents Require compat.
+From Stdlib Require All.
diff --git a/subcomponents/arith.v b/subcomponents/arith.v
new file mode 100644
index 0000000000..01cd4db18e
--- /dev/null
+++ b/subcomponents/arith.v
@@ -0,0 +1,2 @@
+From subcomponents Require ring.
+From Stdlib Require Arith.Arith.
diff --git a/subcomponents/arith_base.v b/subcomponents/arith_base.v
new file mode 100644
index 0000000000..4a3e011642
--- /dev/null
+++ b/subcomponents/arith_base.v
@@ -0,0 +1,54 @@
+From subcomponents Require structures.
+From Stdlib Require Arith.Arith_base.
+From Stdlib Require Arith.Between.
+From Stdlib Require Arith.Bool_nat.
+From Stdlib Require Arith.Cantor.
+From Stdlib Require Arith.Compare.
+From Stdlib Require Arith.Compare_dec.
+From Stdlib Require Arith.EqNat.
+From Stdlib Require Arith.Euclid.
+From Stdlib Require Arith.Factorial.
+From Stdlib Require Arith.PeanoNat.
+From Stdlib Require Arith.Peano_dec.
+From Stdlib Require Arith.Wf_nat.
+From Stdlib Require Arith.Zerob.
+From Stdlib Require Numbers.NumPrelude.
+From Stdlib Require Numbers.NatInt.NZBase.
+From Stdlib Require Numbers.NatInt.NZOrder.
+From Stdlib Require Numbers.NatInt.NZProperties.
+From Stdlib Require Numbers.NatInt.NZDiv.
+From Stdlib Require Numbers.NatInt.NZParity.
+From Stdlib Require Numbers.NatInt.NZPow.
+From Stdlib Require Numbers.NatInt.NZSqrt.
+From Stdlib Require Numbers.NatInt.NZGcd.
+From Stdlib Require Numbers.NatInt.NZBits.
+From Stdlib Require Numbers.NatInt.NZDomain.
+From Stdlib Require Numbers.NatInt.NZAxioms.
+From Stdlib Require Numbers.NatInt.NZAddOrder.
+From Stdlib Require Numbers.NatInt.NZMul.
+From Stdlib Require Numbers.NatInt.NZLog.
+From Stdlib Require Numbers.NatInt.NZAdd.
+From Stdlib Require Numbers.NatInt.NZMulOrder.
+From Stdlib Require Numbers.Natural.Abstract.NStrongRec.
+From Stdlib Require Numbers.Natural.Abstract.NAdd.
+From Stdlib Require Numbers.Natural.Abstract.NAxioms.
+From Stdlib Require Numbers.Natural.Abstract.NDefOps.
+From Stdlib Require Numbers.Natural.Abstract.NSqrt.
+From Stdlib Require Numbers.Natural.Abstract.NDiv0.
+From Stdlib Require Numbers.Natural.Abstract.NBits.
+From Stdlib Require Numbers.Natural.Abstract.NGcd.
+From Stdlib Require Numbers.Natural.Abstract.NParity.
+From Stdlib Require Numbers.Natural.Abstract.NProperties.
+From Stdlib Require Numbers.Natural.Abstract.NMaxMin.
+From Stdlib Require Numbers.Natural.Abstract.NDiv.
+From Stdlib Require Numbers.Natural.Abstract.NPow.
+From Stdlib Require Numbers.Natural.Abstract.NAddOrder.
+From Stdlib Require Numbers.Natural.Abstract.NLcm0.
+From Stdlib Require Numbers.Natural.Abstract.NLog.
+From Stdlib Require Numbers.Natural.Abstract.NMulOrder.
+From Stdlib Require Numbers.Natural.Abstract.NIso.
+From Stdlib Require Numbers.Natural.Abstract.NSub.
+From Stdlib Require Numbers.Natural.Abstract.NBase.
+From Stdlib Require Numbers.Natural.Abstract.NLcm.
+From Stdlib Require Numbers.Natural.Abstract.NOrder.
+From Stdlib Require Classes.SetoidDec.
diff --git a/subcomponents/bool.v b/subcomponents/bool.v
new file mode 100644
index 0000000000..47bb072b7c
--- /dev/null
+++ b/subcomponents/bool.v
@@ -0,0 +1,5 @@
+From subcomponents Require classes.
+From Stdlib Require Bool.IfProp.
+From Stdlib Require Bool.Bool.
+From Stdlib Require Bool.DecBool.
+From Stdlib Require Bool.BoolEq.
diff --git a/subcomponents/classes.v b/subcomponents/classes.v
new file mode 100644
index 0000000000..97aa4bc80a
--- /dev/null
+++ b/subcomponents/classes.v
@@ -0,0 +1,7 @@
+From subcomponents Require program.
+From subcomponents Require relations.
+From Stdlib Require Classes.CEquivalence.
+From Stdlib Require Classes.DecidableClass.
+From Stdlib Require Classes.Morphisms_Relations.
+From Stdlib Require Classes.RelationPairs.
+From Stdlib Require Classes.SetoidClass.
diff --git a/subcomponents/classical_logic.v b/subcomponents/classical_logic.v
new file mode 100644
index 0000000000..0f49cbf346
--- /dev/null
+++ b/subcomponents/classical_logic.v
@@ -0,0 +1,16 @@
+From subcomponents Require arith.
+From Stdlib Require Logic.IndefiniteDescription.
+From Stdlib Require Logic.Classical_Pred_Type.
+From Stdlib Require Logic.Classical_Prop.
+From Stdlib Require Logic.ClassicalFacts.
+From Stdlib Require Logic.Classical.
+From Stdlib Require Logic.Epsilon.
+From Stdlib Require Logic.ClassicalChoice.
+From Stdlib Require Logic.Description.
+From Stdlib Require Logic.ClassicalEpsilon.
+From Stdlib Require Logic.ChoiceFacts.
+From Stdlib Require Logic.PropExtensionality.
+From Stdlib Require Logic.ClassicalDescription.
+From Stdlib Require Logic.ClassicalUniqueChoice.
+From Stdlib Require Logic.SetoidChoice.
+From Stdlib Require Logic.Diaconescu.
diff --git a/subcomponents/compat.v b/subcomponents/compat.v
new file mode 100644
index 0000000000..f25ed48b07
--- /dev/null
+++ b/subcomponents/compat.v
@@ -0,0 +1,11 @@
+From subcomponents Require rtauto.
+From subcomponents Require fmaps_fsets_msets.
+From subcomponents Require funind.
+From subcomponents Require extraction.
+From subcomponents Require reals.
+From subcomponents Require zmod.
+From subcomponents Require wellfounded.
+From subcomponents Require streams.
+From Stdlib Require Compat.AdmitAxiom.
+From Stdlib Require Compat.Stdlib818.
+From Stdlib Require Reals.Nsatz.
diff --git a/subcomponents/corelib_wrapper.v b/subcomponents/corelib_wrapper.v
new file mode 100644
index 0000000000..7ce6279b14
--- /dev/null
+++ b/subcomponents/corelib_wrapper.v
@@ -0,0 +1,62 @@
+From Stdlib Require Array.ArrayAxioms.
+From Stdlib Require Array.PrimArray.
+From Stdlib Require BinNums.IntDef.
+From Stdlib Require BinNums.NatDef.
+From Stdlib Require BinNums.PosDef.
+From Stdlib Require Classes.CMorphisms.
+From Stdlib Require Classes.CRelationClasses.
+From Stdlib Require Classes.Equivalence.
+From Stdlib Require Classes.Init.
+From Stdlib Require Classes.Morphisms.
+From Stdlib Require Classes.Morphisms_Prop.
+From Stdlib Require Classes.RelationClasses.
+From Stdlib Require Classes.SetoidTactics.
+From Stdlib Require Compat.Coq818.
+From Stdlib Require Compat.Coq819.
+From Stdlib Require Compat.Coq820.
+From Stdlib Require Floats.FloatAxioms.
+From Stdlib Require Floats.FloatClass.
+From Stdlib Require Floats.FloatOps.
+From Stdlib Require Floats.PrimFloat.
+From Stdlib Require Floats.SpecFloat.
+From Stdlib Require Init.Byte.
+From Stdlib Require Init.Datatypes.
+From Stdlib Require Init.Decimal.
+From Stdlib Require Init.Hexadecimal.
+From Stdlib Require Init.Logic.
+From Stdlib Require Init.Ltac.
+From Stdlib Require Init.Nat.
+From Stdlib Require Init.Notations.
+From Stdlib Require Init.Number.
+From Stdlib Require Init.Peano.
+From Stdlib Require Init.Prelude.
+From Stdlib Require Init.Specif.
+From Stdlib Require Init.Sumbool.
+From Stdlib Require Init.Tactics.
+From Stdlib Require Init.Tauto.
+From Stdlib Require Init.Wf.
+From Stdlib Require Lists.ListDef.
+From Stdlib Require Numbers.BinNums.
+From Stdlib Require Numbers.Cyclic.Int63.CarryType.
+From Stdlib Require Numbers.Cyclic.Int63.PrimInt63.
+From Stdlib Require Numbers.Cyclic.Int63.Sint63Axioms.
+From Stdlib Require Numbers.Cyclic.Int63.Uint63Axioms.
+From Stdlib Require Program.Basics.
+From Stdlib Require Program.Tactics.
+From Stdlib Require Program.Utils.
+From Stdlib Require Program.Wf.
+From Stdlib Require Relations.Relation_Definitions.
+From Stdlib Require Setoids.Setoid.
+From Stdlib Require Strings.PrimString.
+From Stdlib Require Strings.PrimStringAxioms.
+From Stdlib Require derive.Derive.
+From Stdlib Require extraction.ExtrHaskellBasic.
+From Stdlib Require extraction.ExtrOcamlBasic.
+From Stdlib Require extraction.Extraction.
+From Stdlib Require ssr.ssrbool.
+From Stdlib Require ssr.ssrclasses.
+From Stdlib Require ssr.ssreflect.
+From Stdlib Require ssr.ssrfun.
+From Stdlib Require ssr.ssrsetoid.
+From Stdlib Require ssr.ssrunder.
+From Stdlib Require ssrmatching.ssrmatching.
diff --git a/subcomponents/extraction.v b/subcomponents/extraction.v
new file mode 100644
index 0000000000..9b02aaf76a
--- /dev/null
+++ b/subcomponents/extraction.v
@@ -0,0 +1,22 @@
+From subcomponents Require primitive_string.
+From subcomponents Require primitive_array.
+From subcomponents Require primitive_floats.
+From Stdlib Require extraction.ExtrHaskellZInteger.
+From Stdlib Require extraction.ExtrHaskellZInt.
+From Stdlib Require extraction.ExtrHaskellNatNum.
+From Stdlib Require extraction.ExtrHaskellString.
+From Stdlib Require extraction.ExtrOcamlZInt.
+From Stdlib Require extraction.ExtrOcamlNativeString.
+From Stdlib Require extraction.ExtrOCamlFloats.
+From Stdlib Require extraction.ExtrOcamlNatBigInt.
+From Stdlib Require extraction.ExtrOcamlZBigInt.
+From Stdlib Require extraction.ExtrOcamlNatInt.
+From Stdlib Require extraction.ExtrHaskellNatInt.
+From Stdlib Require extraction.ExtrOcamlString.
+From Stdlib Require extraction.ExtrOCamlPString.
+From Stdlib Require extraction.ExtrHaskellZNum.
+From Stdlib Require extraction.ExtrOcamlChar.
+From Stdlib Require extraction.ExtrOCamlPArray.
+From Stdlib Require extraction.ExtrOcamlIntConv.
+From Stdlib Require extraction.ExtrOCamlInt63.
+From Stdlib Require extraction.ExtrHaskellNatInteger.
diff --git a/subcomponents/field.v b/subcomponents/field.v
new file mode 100644
index 0000000000..54175ff749
--- /dev/null
+++ b/subcomponents/field.v
@@ -0,0 +1,2 @@
+From subcomponents Require zarith.
+From Stdlib Require setoid_ring.Field.
diff --git a/subcomponents/fmaps_fsets_msets.v b/subcomponents/fmaps_fsets_msets.v
new file mode 100644
index 0000000000..e2701728be
--- /dev/null
+++ b/subcomponents/fmaps_fsets_msets.v
@@ -0,0 +1,36 @@
+From subcomponents Require orders_ex.
+From subcomponents Require zarith.
+From Stdlib Require FSets.FMapInterface.
+From Stdlib Require FSets.FSetInterface.
+From Stdlib Require FSets.FSetWeakList.
+From Stdlib Require FSets.FSetAVL.
+From Stdlib Require FSets.FSetCompat.
+From Stdlib Require FSets.FSetDecide.
+From Stdlib Require FSets.FSetList.
+From Stdlib Require FSets.FSetProperties.
+From Stdlib Require FSets.FMapList.
+From Stdlib Require FSets.FMapFacts.
+From Stdlib Require FSets.FSetPositive.
+From Stdlib Require FSets.FMapFullAVL.
+From Stdlib Require FSets.FSetToFiniteSet.
+From Stdlib Require FSets.FMapAVL.
+From Stdlib Require FSets.FMapPositive.
+From Stdlib Require FSets.FSets.
+From Stdlib Require FSets.FMaps.
+From Stdlib Require FSets.FSetFacts.
+From Stdlib Require FSets.FSetEqProperties.
+From Stdlib Require FSets.FSetBridge.
+From Stdlib Require FSets.FMapWeakList.
+From Stdlib Require MSets.MSetList.
+From Stdlib Require MSets.MSetDecide.
+From Stdlib Require MSets.MSets.
+From Stdlib Require MSets.MSetWeakList.
+From Stdlib Require MSets.MSetGenTree.
+From Stdlib Require MSets.MSetAVL.
+From Stdlib Require MSets.MSetInterface.
+From Stdlib Require MSets.MSetFacts.
+From Stdlib Require MSets.MSetProperties.
+From Stdlib Require MSets.MSetRBT.
+From Stdlib Require MSets.MSetPositive.
+From Stdlib Require MSets.MSetToFiniteSet.
+From Stdlib Require MSets.MSetEqProperties.
diff --git a/subcomponents/funind.v b/subcomponents/funind.v
new file mode 100644
index 0000000000..b1a690f2b1
--- /dev/null
+++ b/subcomponents/funind.v
@@ -0,0 +1,3 @@
+From subcomponents Require arith_base.
+From Stdlib Require funind.FunInd.
+From Stdlib Require funind.Recdef.
diff --git a/subcomponents/lia.v b/subcomponents/lia.v
new file mode 100644
index 0000000000..43c5e157d0
--- /dev/null
+++ b/subcomponents/lia.v
@@ -0,0 +1,25 @@
+From subcomponents Require arith.
+From subcomponents Require narith.
+From Stdlib Require omega.OmegaLemmas.
+From Stdlib Require omega.PreOmega.
+From Stdlib Require micromega.ZifyN.
+From Stdlib Require micromega.ZifyComparison.
+From Stdlib Require micromega.ZifyClasses.
+From Stdlib Require micromega.ZifyNat.
+From Stdlib Require micromega.ZifyPow.
+From Stdlib Require micromega.ZifyBool.
+From Stdlib Require micromega.Zify.
+From Stdlib Require micromega.ZifyInst.
+From Stdlib Require micromega.DeclConstantZ.
+From Stdlib Require micromega.OrderedRing.
+From Stdlib Require micromega.Tauto.
+From Stdlib Require micromega.Env.
+From Stdlib Require micromega.Refl.
+From Stdlib Require micromega.ZArith_hints.
+From Stdlib Require micromega.ZMicromega.
+From Stdlib Require micromega.EnvRing.
+From Stdlib Require micromega.Lia.
+From Stdlib Require micromega.VarMap.
+From Stdlib Require micromega.Ztac.
+From Stdlib Require micromega.ZCoeff.
+From Stdlib Require micromega.RingMicromega.
diff --git a/subcomponents/lists.v b/subcomponents/lists.v
new file mode 100644
index 0000000000..019e4551d4
--- /dev/null
+++ b/subcomponents/lists.v
@@ -0,0 +1,8 @@
+From subcomponents Require arith_base.
+From Stdlib Require Lists.ListDec.
+From Stdlib Require Lists.List.
+From Stdlib Require Lists.ListSet.
+From Stdlib Require Lists.ListTactics.
+From Stdlib Require Numbers.NaryFunctions.
+From Stdlib Require Logic.WKL.
+From Stdlib Require Classes.EquivDec.
diff --git a/subcomponents/logic.v b/subcomponents/logic.v
new file mode 100644
index 0000000000..6febd1851c
--- /dev/null
+++ b/subcomponents/logic.v
@@ -0,0 +1,22 @@
+From Stdlib Require Logic.Adjointification.
+From Stdlib Require Logic.Eqdep_dec.
+From Stdlib Require Logic.JMeq.
+From Stdlib Require Logic.SetIsType.
+From Stdlib Require Logic.Berardi.
+From Stdlib Require Logic.ExtensionalFunctionRepresentative.
+From Stdlib Require Logic.ProofIrrelevanceFacts.
+From Stdlib Require Logic.StrictProp.
+From Stdlib Require Logic.ConstructiveEpsilon.
+From Stdlib Require Logic.ExtensionalityFacts.
+From Stdlib Require Logic.ProofIrrelevance.
+From Stdlib Require Logic.WeakFan.
+From Stdlib Require Logic.Decidable.
+From Stdlib Require Logic.FunctionalExtensionality.
+From Stdlib Require Logic.PropExtensionalityFacts.
+From Stdlib Require Logic.Eqdep.
+From Stdlib Require Logic.HLevelsBase.
+From Stdlib Require Logic.HLevels.
+From Stdlib Require Logic.PropFacts.
+From Stdlib Require Logic.EqdepFacts.
+From Stdlib Require Logic.Hurkens.
+From Stdlib Require Logic.RelationalChoice.
diff --git a/subcomponents/lqa.v b/subcomponents/lqa.v
new file mode 100644
index 0000000000..48740a4a8f
--- /dev/null
+++ b/subcomponents/lqa.v
@@ -0,0 +1,8 @@
+From subcomponents Require field.
+From subcomponents Require qarith_base.
+From Stdlib Require micromega.QMicromega.
+From Stdlib Require micromega.Lqa.
+From Stdlib Require micromega.DeclConstant.
+From Stdlib Require QArith.Qfield.
+From Stdlib Require QArith.Qring.
+From Stdlib Require setoid_ring.Rings_Q.
diff --git a/subcomponents/narith.v b/subcomponents/narith.v
new file mode 100644
index 0000000000..cb5d4a7a26
--- /dev/null
+++ b/subcomponents/narith.v
@@ -0,0 +1,2 @@
+From subcomponents Require ring.
+From Stdlib Require NArith.NArith.
diff --git a/subcomponents/narith_base.v b/subcomponents/narith_base.v
new file mode 100644
index 0000000000..7ce0557ccb
--- /dev/null
+++ b/subcomponents/narith_base.v
@@ -0,0 +1,9 @@
+From subcomponents Require positive.
+From Stdlib Require NArith.BinNatDef.
+From Stdlib Require NArith.BinNat.
+From Stdlib Require NArith.Nnat.
+From Stdlib Require NArith.Ndiv_def.
+From Stdlib Require NArith.Ndec.
+From Stdlib Require NArith.Ngcd_def.
+From Stdlib Require NArith.Nsqrt_def.
+From Stdlib Require NArith.NArith_base.
diff --git a/subcomponents/orders_ex.v b/subcomponents/orders_ex.v
new file mode 100644
index 0000000000..f327ab46b2
--- /dev/null
+++ b/subcomponents/orders_ex.v
@@ -0,0 +1,12 @@
+From subcomponents Require strings.
+From subcomponents Require sorting.
+From Stdlib Require Structures.BoolOrder.
+From Stdlib Require Structures.OrdersEx.
+From Stdlib Require Structures.OrdersLists.
+From Stdlib Require Structures.EqualitiesFacts.
+From Stdlib Require Structures.OrderedTypeAlt.
+From Stdlib Require Structures.OrderedType.
+From Stdlib Require Structures.DecidableType.
+From Stdlib Require Structures.OrderedTypeEx.
+From Stdlib Require Structures.OrdersAlt.
+From Stdlib Require Structures.DecidableTypeEx.
diff --git a/subcomponents/positive.v b/subcomponents/positive.v
new file mode 100644
index 0000000000..48b04de0ca
--- /dev/null
+++ b/subcomponents/positive.v
@@ -0,0 +1,7 @@
+From subcomponents Require arith_base.
+From Stdlib Require Numbers.AltBinNotations.
+From Stdlib Require PArith.Pnat.
+From Stdlib Require PArith.POrderedType.
+From Stdlib Require PArith.BinPos.
+From Stdlib Require PArith.PArith.
+From Stdlib Require PArith.BinPosDef.
diff --git a/subcomponents/primitive_array.v b/subcomponents/primitive_array.v
new file mode 100644
index 0000000000..3da0801e96
--- /dev/null
+++ b/subcomponents/primitive_array.v
@@ -0,0 +1,2 @@
+From subcomponents Require primitive_int.
+From Stdlib Require Array.PArray.
diff --git a/subcomponents/primitive_floats.v b/subcomponents/primitive_floats.v
new file mode 100644
index 0000000000..829b5c5b5e
--- /dev/null
+++ b/subcomponents/primitive_floats.v
@@ -0,0 +1,3 @@
+From subcomponents Require primitive_int.
+From Stdlib Require Floats.Floats.
+From Stdlib Require Floats.FloatLemmas.
diff --git a/subcomponents/primitive_int.v b/subcomponents/primitive_int.v
new file mode 100644
index 0000000000..2be28cb64d
--- /dev/null
+++ b/subcomponents/primitive_int.v
@@ -0,0 +1,11 @@
+From subcomponents Require unicode.
+From subcomponents Require zarith.
+From Stdlib Require Numbers.Cyclic.Int63.Sint63.
+From Stdlib Require Numbers.Cyclic.Int63.Cyclic63.
+From Stdlib Require Numbers.Cyclic.Int63.Uint63.
+From Stdlib Require Numbers.Cyclic.Int63.Ring63.
+From Stdlib Require Numbers.Cyclic.Abstract.NZCyclic.
+From Stdlib Require Numbers.Cyclic.Abstract.DoubleType.
+From Stdlib Require Numbers.Cyclic.Abstract.CyclicAxioms.
+From Stdlib Require micromega.ZifyUint63.
+From Stdlib Require micromega.ZifySint63.
diff --git a/subcomponents/primitive_string.v b/subcomponents/primitive_string.v
new file mode 100644
index 0000000000..ba7447015f
--- /dev/null
+++ b/subcomponents/primitive_string.v
@@ -0,0 +1,3 @@
+From subcomponents Require primitive_int.
+From subcomponents Require orders_ex.
+From Stdlib Require Strings.PString.
diff --git a/subcomponents/program.v b/subcomponents/program.v
new file mode 100644
index 0000000000..fe2dcd81c4
--- /dev/null
+++ b/subcomponents/program.v
@@ -0,0 +1,3 @@
+From subcomponents Require corelib_wrapper.
+From subcomponents Require logic.
+From Stdlib Require Program.Program.
diff --git a/subcomponents/qarith.v b/subcomponents/qarith.v
new file mode 100644
index 0000000000..01e6ae269e
--- /dev/null
+++ b/subcomponents/qarith.v
@@ -0,0 +1,10 @@
+From subcomponents Require lqa.
+From Stdlib Require QArith.Qcabs.
+From Stdlib Require QArith.Qround.
+From Stdlib Require QArith.Qabs.
+From Stdlib Require QArith.QArith.
+From Stdlib Require QArith.Qpower.
+From Stdlib Require QArith.Qcanon.
+From Stdlib Require QArith.QNsatz.
+From Stdlib Require Numbers.DecimalQ.
+From Stdlib Require Numbers.HexadecimalQ.
diff --git a/subcomponents/qarith_base.v b/subcomponents/qarith_base.v
new file mode 100644
index 0000000000..36a87cb83f
--- /dev/null
+++ b/subcomponents/qarith_base.v
@@ -0,0 +1,5 @@
+From subcomponents Require ring.
+From Stdlib Require QArith.Qreduction.
+From Stdlib Require QArith.Qminmax.
+From Stdlib Require QArith.QOrderedType.
+From Stdlib Require QArith.QArith_base.
diff --git a/subcomponents/reals.v b/subcomponents/reals.v
new file mode 100644
index 0000000000..e7b92effa1
--- /dev/null
+++ b/subcomponents/reals.v
@@ -0,0 +1,16 @@
+From subcomponents Require qarith.
+From subcomponents Require classical_logic.
+From subcomponents Require vectors.
+From Stdlib Require Reals.Reals.
+From Stdlib Require Reals.Abstract.ConstructivePower.
+From Stdlib Require Reals.Abstract.ConstructiveMinMax.
+From Stdlib Require Reals.Runcountable.
+From Stdlib Require Reals.ClassicalConstructiveReals.
+From Stdlib Require Reals.Machin.
+From Stdlib Require Reals.Rminmax.
+From Stdlib Require Reals.Rlogic.
+From Stdlib Require Reals.Nsatz.
+From Stdlib Require setoid_ring.Rings_R.
+From Stdlib Require micromega.Psatz.
+From Stdlib Require Numbers.DecimalR.
+From Stdlib Require Numbers.HexadecimalR.
diff --git a/subcomponents/relations.v b/subcomponents/relations.v
new file mode 100644
index 0000000000..de5bc04a43
--- /dev/null
+++ b/subcomponents/relations.v
@@ -0,0 +1,4 @@
+From subcomponents Require corelib_wrapper.
+From Stdlib Require Relations.Relation_Operators.
+From Stdlib Require Relations.Operators_Properties.
+From Stdlib Require Relations.Relations.
diff --git a/subcomponents/ring.v b/subcomponents/ring.v
new file mode 100644
index 0000000000..8930df5ba5
--- /dev/null
+++ b/subcomponents/ring.v
@@ -0,0 +1,24 @@
+From subcomponents Require zarith_base.
+From subcomponents Require lists.
+From Stdlib Require ZArith.Zpow_def.
+From Stdlib Require ZArith.Zcomplements.
+From Stdlib Require ZArith.Zdiv.
+From Stdlib Require setoid_ring.Ncring_polynom.
+From Stdlib Require setoid_ring.Rings_Z.
+From Stdlib Require setoid_ring.Ncring_initial.
+From Stdlib Require setoid_ring.Ring_polynom.
+From Stdlib Require setoid_ring.ZArithRing.
+From Stdlib Require setoid_ring.Integral_domain.
+From Stdlib Require setoid_ring.Ring_base.
+From Stdlib Require setoid_ring.BinList.
+From Stdlib Require setoid_ring.Ncring.
+From Stdlib Require setoid_ring.Ring.
+From Stdlib Require setoid_ring.Algebra_syntax.
+From Stdlib Require setoid_ring.InitialRing.
+From Stdlib Require setoid_ring.Cring.
+From Stdlib Require setoid_ring.Ncring_tac.
+From Stdlib Require setoid_ring.Ring_tac.
+From Stdlib Require setoid_ring.ArithRing.
+From Stdlib Require setoid_ring.NArithRing.
+From Stdlib Require setoid_ring.Ring_theory.
+From Stdlib Require nsatz.NsatzTactic.
diff --git a/subcomponents/rtauto.v b/subcomponents/rtauto.v
new file mode 100644
index 0000000000..f80fef364f
--- /dev/null
+++ b/subcomponents/rtauto.v
@@ -0,0 +1,4 @@
+From subcomponents Require positive.
+From subcomponents Require lists.
+From Stdlib Require rtauto.Bintree.
+From Stdlib Require rtauto.Rtauto.
diff --git a/subcomponents/sets.v b/subcomponents/sets.v
new file mode 100644
index 0000000000..eb2cc874d4
--- /dev/null
+++ b/subcomponents/sets.v
@@ -0,0 +1,23 @@
+From subcomponents Require classical_logic.
+From Stdlib Require Sets.Partial_Order.
+From Stdlib Require Sets.Multiset.
+From Stdlib Require Sets.Uniset.
+From Stdlib Require Sets.Relations_2.
+From Stdlib Require Sets.Image.
+From Stdlib Require Sets.Relations_3.
+From Stdlib Require Sets.Relations_1.
+From Stdlib Require Sets.Classical_sets.
+From Stdlib Require Sets.Finite_sets.
+From Stdlib Require Sets.Permut.
+From Stdlib Require Sets.Integers.
+From Stdlib Require Sets.Finite_sets_facts.
+From Stdlib Require Sets.Powerset_facts.
+From Stdlib Require Sets.Powerset.
+From Stdlib Require Sets.Powerset_Classical_facts.
+From Stdlib Require Sets.Ensembles.
+From Stdlib Require Sets.Relations_1_facts.
+From Stdlib Require Sets.Constructive_sets.
+From Stdlib Require Sets.Infinite_sets.
+From Stdlib Require Sets.Relations_2_facts.
+From Stdlib Require Sets.Relations_3_facts.
+From Stdlib Require Sets.Cpo.
diff --git a/subcomponents/sorting.v b/subcomponents/sorting.v
new file mode 100644
index 0000000000..5368370346
--- /dev/null
+++ b/subcomponents/sorting.v
@@ -0,0 +1,13 @@
+From subcomponents Require lia.
+From subcomponents Require sets.
+From subcomponents Require vectors.
+From Stdlib Require Sorting.Heap.
+From Stdlib Require Sorting.CPermutation.
+From Stdlib Require Sorting.Mergesort.
+From Stdlib Require Sorting.PermutSetoid.
+From Stdlib Require Sorting.PermutEq.
+From Stdlib Require Sorting.Sorting.
+From Stdlib Require Sorting.Permutation.
+From Stdlib Require Sorting.Sorted.
+From Stdlib Require Sorting.SetoidList.
+From Stdlib Require Sorting.SetoidPermutation.
diff --git a/subcomponents/streams.v b/subcomponents/streams.v
new file mode 100644
index 0000000000..5718dde392
--- /dev/null
+++ b/subcomponents/streams.v
@@ -0,0 +1,3 @@
+From subcomponents Require logic.
+From Stdlib Require Streams.Streams.
+From Stdlib Require Streams.StreamMemo.
diff --git a/subcomponents/strings.v b/subcomponents/strings.v
new file mode 100644
index 0000000000..9a80dbe351
--- /dev/null
+++ b/subcomponents/strings.v
@@ -0,0 +1,9 @@
+From subcomponents Require arith.
+From Stdlib Require Strings.HexString.
+From Stdlib Require Strings.Ascii.
+From Stdlib Require Strings.String.
+From Stdlib Require Strings.OctalString.
+From Stdlib Require Strings.Byte.
+From Stdlib Require Strings.BinaryString.
+From Stdlib Require Numbers.DecimalString.
+From Stdlib Require Numbers.HexadecimalString.
diff --git a/subcomponents/structures.v b/subcomponents/structures.v
new file mode 100644
index 0000000000..ca746e1c2c
--- /dev/null
+++ b/subcomponents/structures.v
@@ -0,0 +1,6 @@
+From subcomponents Require bool.
+From Stdlib Require Structures.GenericMinMax.
+From Stdlib Require Structures.Equalities.
+From Stdlib Require Structures.Orders.
+From Stdlib Require Structures.OrdersFacts.
+From Stdlib Require Structures.OrdersTac.
diff --git a/subcomponents/unicode.v b/subcomponents/unicode.v
new file mode 100644
index 0000000000..635ac7137c
--- /dev/null
+++ b/subcomponents/unicode.v
@@ -0,0 +1,2 @@
+From Stdlib Require Unicode.Utf8_core.
+From Stdlib Require Unicode.Utf8.
diff --git a/subcomponents/vectors.v b/subcomponents/vectors.v
new file mode 100644
index 0000000000..cf98d049a0
--- /dev/null
+++ b/subcomponents/vectors.v
@@ -0,0 +1,8 @@
+From subcomponents Require lists.
+From Stdlib Require Vectors.VectorEq.
+From Stdlib Require Vectors.VectorDef.
+From Stdlib Require Vectors.Vector.
+From Stdlib Require Vectors.Fin.
+From Stdlib Require Vectors.VectorSpec.
+From Stdlib Require Vectors.Bvector.
+From Stdlib Require Vectors.FinFun.
diff --git a/subcomponents/wellfounded.v b/subcomponents/wellfounded.v
new file mode 100644
index 0000000000..54e991ea5a
--- /dev/null
+++ b/subcomponents/wellfounded.v
@@ -0,0 +1,11 @@
+From subcomponents Require lists.
+From Stdlib Require Wellfounded.Inclusion.
+From Stdlib Require Wellfounded.Wellfounded.
+From Stdlib Require Wellfounded.Union.
+From Stdlib Require Wellfounded.Transitive_Closure.
+From Stdlib Require Wellfounded.Well_Ordering.
+From Stdlib Require Wellfounded.Inverse_Image.
+From Stdlib Require Wellfounded.Disjoint_Union.
+From Stdlib Require Wellfounded.Lexicographic_Product.
+From Stdlib Require Wellfounded.Lexicographic_Exponentiation.
+From Stdlib Require Wellfounded.List_Extension.
diff --git a/subcomponents/zarith.v b/subcomponents/zarith.v
new file mode 100644
index 0000000000..cf7d6cf8b6
--- /dev/null
+++ b/subcomponents/zarith.v
@@ -0,0 +1,9 @@
+From subcomponents Require lia.
+From Stdlib Require ZArith.ZArith.
+From Stdlib Require ZArith.Zquot.
+From Stdlib Require Numbers.Natural.Binary.NBinary.
+From Stdlib Require ZArith.Zwf.
+From Stdlib Require Numbers.Integer.Binary.ZBinary.
+From Stdlib Require Numbers.Integer.NatPairs.ZNatPairs.
+From Stdlib Require Numbers.DecimalNat.
+From Stdlib Require Numbers.HexadecimalNat.
diff --git a/subcomponents/zarith_base.v b/subcomponents/zarith_base.v
new file mode 100644
index 0000000000..2da4e7d1a2
--- /dev/null
+++ b/subcomponents/zarith_base.v
@@ -0,0 +1,39 @@
+From subcomponents Require narith_base.
+From Stdlib Require Numbers.Integer.Abstract.ZSgnAbs.
+From Stdlib Require Numbers.Integer.Abstract.ZAxioms.
+From Stdlib Require Numbers.Integer.Abstract.ZAddOrder.
+From Stdlib Require Numbers.Integer.Abstract.ZProperties.
+From Stdlib Require Numbers.Integer.Abstract.ZDivTrunc.
+From Stdlib Require Numbers.Integer.Abstract.ZParity.
+From Stdlib Require Numbers.Integer.Abstract.ZMul.
+From Stdlib Require Numbers.Integer.Abstract.ZPow.
+From Stdlib Require Numbers.Integer.Abstract.ZAdd.
+From Stdlib Require Numbers.Integer.Abstract.ZDivFloor.
+From Stdlib Require Numbers.Integer.Abstract.ZMulOrder.
+From Stdlib Require Numbers.Integer.Abstract.ZDivEucl.
+From Stdlib Require Numbers.Integer.Abstract.ZMaxMin.
+From Stdlib Require Numbers.Integer.Abstract.ZGcd.
+From Stdlib Require Numbers.Integer.Abstract.ZLt.
+From Stdlib Require Numbers.Integer.Abstract.ZLcm.
+From Stdlib Require Numbers.Integer.Abstract.ZBase.
+From Stdlib Require Numbers.Integer.Abstract.ZBits.
+From Stdlib Require ZArith.BinIntDef.
+From Stdlib Require ZArith.BinInt.
+From Stdlib Require ZArith.Zcompare.
+From Stdlib Require ZArith.Zorder.
+From Stdlib Require ZArith.Zminmax.
+From Stdlib Require ZArith.Zmin.
+From Stdlib Require ZArith.Zmax.
+From Stdlib Require ZArith.Znat.
+From Stdlib Require ZArith.ZArith_dec.
+From Stdlib Require ZArith.Zabs.
+From Stdlib Require ZArith.auxiliary.
+From Stdlib Require ZArith.Zbool.
+From Stdlib Require ZArith.Zmisc.
+From Stdlib Require ZArith.Wf_Z.
+From Stdlib Require ZArith.Zhints.
+From Stdlib Require ZArith.ZArith_base.
+From Stdlib Require ZArith.Zeven.
+From Stdlib Require ZArith.Zpow_alt.
+From Stdlib Require ZArith.Zeuclid.
+From Stdlib Require ZArith.Int.
diff --git a/subcomponents/zmod.v b/subcomponents/zmod.v
new file mode 100644
index 0000000000..ef281ee3db
--- /dev/null
+++ b/subcomponents/zmod.v
@@ -0,0 +1,6 @@
+From subcomponents Require zarith.
+From subcomponents Require sorting.
+From subcomponents Require field.
+From Stdlib Require Zmod.Bits.
+From Stdlib Require Zmod.Zmod.
+From Stdlib Require Zmod.Zstar.
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 7e6f530e50..314ca240b9 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -30,11 +30,15 @@ else
   export FINDLIB_SEP=:
 endif
 
+# these variables are meant to be overridden if you want to add *extra* flags
 COQEXTRAFLAGS?=
+COQCHKEXTRAFLAGS?=
+
 COQFLAGS?=$(COQEXTRAFLAGS)
+COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS)
 
 coqc := rocq c -q -R prerequisite TestSuite $(COQFLAGS)
-coqchk := rocqchk -R prerequisite TestSuite
+coqchk := rocqchk -R prerequisite TestSuite $(COQCHKFLAGS)
 coqdoc := rocq doc
 coqtop := rocq repl -q -test-mode -R prerequisite TestSuite
 
diff --git a/theories/All.sh b/theories/All.sh
new file mode 100755
index 0000000000..3af10fd526
--- /dev/null
+++ b/theories/All.sh
@@ -0,0 +1,8 @@
+#!/bin/sh
+set -e
+set -u
+set -o pipefail
+cd "$(dirname "$0")"
+printf 'Set Warnings "-deprecated-library-file,-warn-library-file,-notation-incompatible-prefix,-notation-overridden,-overwriting-delimiting-key".\n'
+find . -name '*.v' ! -path ./All.v | sort | xargs rocq dep -Q . Stdlib -sort | \
+  sed -e 's#\./#From Stdlib Require Export #g' -e 's#\.v\s*#.\n#g' -e 's#/#.#g'
diff --git a/theories/All/All.v b/theories/All/All.v
deleted file mode 100644
index 4b619a5d94..0000000000
--- a/theories/All/All.v
+++ /dev/null
@@ -1,580 +0,0 @@
-Set Warnings "-deprecated-library-file,-warn-library-file,-notation-incompatible-prefix,-notation-overridden,-overwriting-delimiting-key".
-
-From Stdlib Require Export ssrmatching.ssrmatching.
-From Stdlib Require Export ssr.ssrbool.
-From Stdlib Require Export ssr.ssrclasses.
-From Stdlib Require Export ssr.ssreflect.
-From Stdlib Require Export ssr.ssrfun.
-From Stdlib Require Export ssr.ssrsetoid.
-From Stdlib Require Export ssr.ssrunder.
-From Stdlib Require Export setoid_ring.Algebra_syntax.
-From Stdlib Require Export setoid_ring.ArithRing.
-From Stdlib Require Export setoid_ring.BinList.
-From Stdlib Require Export setoid_ring.Cring.
-From Stdlib Require Export setoid_ring.Field.
-From Stdlib Require Export setoid_ring.Field_tac.
-From Stdlib Require Export setoid_ring.Field_theory.
-From Stdlib Require Export setoid_ring.InitialRing.
-From Stdlib Require Export setoid_ring.Integral_domain.
-From Stdlib Require Export setoid_ring.NArithRing.
-From Stdlib Require Export setoid_ring.Ncring.
-From Stdlib Require Export setoid_ring.Ncring_initial.
-From Stdlib Require Export setoid_ring.Ncring_polynom.
-From Stdlib Require Export setoid_ring.Ncring_tac.
-From Stdlib Require Export setoid_ring.RealField.
-From Stdlib Require Export setoid_ring.Ring.
-From Stdlib Require Export setoid_ring.Ring_base.
-From Stdlib Require Export setoid_ring.Ring_polynom.
-From Stdlib Require Export setoid_ring.Ring_tac.
-From Stdlib Require Export setoid_ring.Ring_theory.
-From Stdlib Require Export setoid_ring.Rings_Q.
-From Stdlib Require Export setoid_ring.Rings_R.
-From Stdlib Require Export setoid_ring.Rings_Z.
-From Stdlib Require Export setoid_ring.ZArithRing.
-From Stdlib Require Export rtauto.Bintree.
-From Stdlib Require Export rtauto.Rtauto.
-From Stdlib Require Export omega.OmegaLemmas.
-From Stdlib Require Export omega.PreOmega.
-From Stdlib Require Export nsatz.NsatzTactic.
-From Stdlib Require Export micromega.DeclConstant.
-From Stdlib Require Export micromega.DeclConstantZ.
-From Stdlib Require Export micromega.Env.
-From Stdlib Require Export micromega.EnvRing.
-From Stdlib Require Export micromega.Fourier.
-From Stdlib Require Export micromega.Fourier_util.
-From Stdlib Require Export micromega.Lia.
-From Stdlib Require Export micromega.Lqa.
-From Stdlib Require Export micromega.Lra.
-From Stdlib Require Export micromega.OrderedRing.
-From Stdlib Require Export micromega.Psatz.
-From Stdlib Require Export micromega.QMicromega.
-From Stdlib Require Export micromega.RMicromega.
-From Stdlib Require Export micromega.Refl.
-From Stdlib Require Export micromega.RingMicromega.
-From Stdlib Require Export micromega.Tauto.
-From Stdlib Require Export micromega.VarMap.
-From Stdlib Require Export micromega.ZArith_hints.
-From Stdlib Require Export micromega.ZCoeff.
-From Stdlib Require Export micromega.ZMicromega.
-From Stdlib Require Export micromega.Zify.
-From Stdlib Require Export micromega.ZifyBool.
-From Stdlib Require Export micromega.ZifyClasses.
-From Stdlib Require Export micromega.ZifyComparison.
-From Stdlib Require Export micromega.ZifyInst.
-From Stdlib Require Export micromega.ZifyN.
-From Stdlib Require Export micromega.ZifyNat.
-From Stdlib Require Export micromega.ZifyPow.
-From Stdlib Require Export micromega.ZifySint63.
-From Stdlib Require Export micromega.ZifyUint63.
-From Stdlib Require Export micromega.Ztac.
-From Stdlib Require Export funind.FunInd.
-From Stdlib Require Export funind.Recdef.
-From Stdlib Require Export extraction.ExtrHaskellBasic.
-From Stdlib Require Export extraction.ExtrHaskellNatInt.
-From Stdlib Require Export extraction.ExtrHaskellNatInteger.
-From Stdlib Require Export extraction.ExtrHaskellNatNum.
-From Stdlib Require Export extraction.ExtrHaskellString.
-From Stdlib Require Export extraction.ExtrHaskellZInt.
-From Stdlib Require Export extraction.ExtrHaskellZInteger.
-From Stdlib Require Export extraction.ExtrHaskellZNum.
-From Stdlib Require Export extraction.ExtrOCamlFloats.
-From Stdlib Require Export extraction.ExtrOCamlInt63.
-From Stdlib Require Export extraction.ExtrOCamlPArray.
-From Stdlib Require Export extraction.ExtrOCamlPString.
-From Stdlib Require Export extraction.ExtrOcamlBasic.
-From Stdlib Require Export extraction.ExtrOcamlChar.
-From Stdlib Require Export extraction.ExtrOcamlIntConv.
-From Stdlib Require Export extraction.ExtrOcamlNatBigInt.
-From Stdlib Require Export extraction.ExtrOcamlNatInt.
-From Stdlib Require Export extraction.ExtrOcamlNativeString.
-From Stdlib Require Export extraction.ExtrOcamlString.
-From Stdlib Require Export extraction.ExtrOcamlZBigInt.
-From Stdlib Require Export extraction.ExtrOcamlZInt.
-From Stdlib Require Export extraction.Extraction.
-From Stdlib Require Export derive.Derive.
-From Stdlib Require Export btauto.Algebra.
-From Stdlib Require Export btauto.Btauto.
-From Stdlib Require Export btauto.Reflect.
-From Stdlib Require Export ZArith.BinInt.
-From Stdlib Require Export ZArith.BinIntDef.
-From Stdlib Require Export ZArith.Int.
-From Stdlib Require Export ZArith.Wf_Z.
-From Stdlib Require Export ZArith.ZArith.
-From Stdlib Require Export ZArith.ZArith_base.
-From Stdlib Require Export ZArith.ZArith_dec.
-From Stdlib Require Export ZArith.Zabs.
-From Stdlib Require Export ZArith.Zbitwise.
-From Stdlib Require Export ZArith.Zbool.
-From Stdlib Require Export ZArith.Zcompare.
-From Stdlib Require Export ZArith.Zcomplements.
-From Stdlib Require Export ZArith.Zcong.
-From Stdlib Require Export ZArith.Zdivisibility.
-From Stdlib Require Export ZArith.Zdiv.
-From Stdlib Require Export ZArith.Zdiv_facts.
-From Stdlib Require Export ZArith.ZModOffset.
-From Stdlib Require Export ZArith.Zeuclid.
-From Stdlib Require Export ZArith.Zeven.
-From Stdlib Require Export ZArith.Zgcd_alt.
-From Stdlib Require Export ZArith.Zhints.
-From Stdlib Require Export ZArith.Zmax.
-From Stdlib Require Export ZArith.Zmin.
-From Stdlib Require Export ZArith.Zminmax.
-From Stdlib Require Export ZArith.Zmisc.
-From Stdlib Require Export ZArith.Znat.
-From Stdlib Require Export ZArith.Znumtheory.
-From Stdlib Require Export ZArith.Zorder.
-From Stdlib Require Export ZArith.Zpow_alt.
-From Stdlib Require Export ZArith.Zpow_def.
-From Stdlib Require Export ZArith.Zpow_facts.
-From Stdlib Require Export ZArith.Zpower.
-From Stdlib Require Export ZArith.Zquot.
-From Stdlib Require Export ZArith.Zwf.
-From Stdlib Require Export ZArith.auxiliary.
-From Stdlib Require Export Wellfounded.Disjoint_Union.
-From Stdlib Require Export Wellfounded.Inclusion.
-From Stdlib Require Export Wellfounded.Inverse_Image.
-From Stdlib Require Export Wellfounded.Lexicographic_Exponentiation.
-From Stdlib Require Export Wellfounded.Lexicographic_Product.
-From Stdlib Require Export Wellfounded.List_Extension.
-From Stdlib Require Export Wellfounded.Transitive_Closure.
-From Stdlib Require Export Wellfounded.Union.
-From Stdlib Require Export Wellfounded.Well_Ordering.
-From Stdlib Require Export Wellfounded.Wellfounded.
-From Stdlib Require Export Vectors.Bvector.
-From Stdlib Require Export Vectors.Fin.
-From Stdlib Require Export Vectors.FinFun.
-From Stdlib Require Export Vectors.Vector.
-From Stdlib Require Export Vectors.VectorDef.
-From Stdlib Require Export Vectors.VectorEq.
-From Stdlib Require Export Vectors.VectorSpec.
-From Stdlib Require Export Unicode.Utf8.
-From Stdlib Require Export Unicode.Utf8_core.
-From Stdlib Require Export Structures.BoolOrder.
-From Stdlib Require Export Structures.DecidableType.
-From Stdlib Require Export Structures.DecidableTypeEx.
-From Stdlib Require Export Structures.Equalities.
-From Stdlib Require Export Structures.EqualitiesFacts.
-From Stdlib Require Export Structures.GenericMinMax.
-From Stdlib Require Export Structures.OrderedType.
-From Stdlib Require Export Structures.OrderedTypeAlt.
-From Stdlib Require Export Structures.OrderedTypeEx.
-From Stdlib Require Export Structures.Orders.
-From Stdlib Require Export Structures.OrdersAlt.
-From Stdlib Require Export Structures.OrdersEx.
-From Stdlib Require Export Structures.OrdersFacts.
-From Stdlib Require Export Structures.OrdersLists.
-From Stdlib Require Export Structures.OrdersTac.
-From Stdlib Require Export Strings.Ascii.
-From Stdlib Require Export Strings.BinaryString.
-From Stdlib Require Export Strings.Byte.
-From Stdlib Require Export Strings.HexString.
-From Stdlib Require Export Strings.OctalString.
-From Stdlib Require Export Strings.PString.
-From Stdlib Require Export Strings.PrimString.
-From Stdlib Require Export Strings.PrimStringAxioms.
-From Stdlib Require Export Strings.String.
-From Stdlib Require Export Streams.StreamMemo.
-From Stdlib Require Export Streams.Streams.
-From Stdlib Require Export Sorting.CPermutation.
-From Stdlib Require Export Sorting.Heap.
-From Stdlib Require Export Sorting.Mergesort.
-From Stdlib Require Export Sorting.PermutEq.
-From Stdlib Require Export Sorting.PermutSetoid.
-From Stdlib Require Export Sorting.Permutation.
-From Stdlib Require Export Sorting.SetoidList.
-From Stdlib Require Export Sorting.SetoidPermutation.
-From Stdlib Require Export Sorting.Sorted.
-From Stdlib Require Export Sorting.Sorting.
-From Stdlib Require Export Sets.Classical_sets.
-From Stdlib Require Export Sets.Constructive_sets.
-From Stdlib Require Export Sets.Cpo.
-From Stdlib Require Export Sets.Ensembles.
-From Stdlib Require Export Sets.Finite_sets.
-From Stdlib Require Export Sets.Finite_sets_facts.
-From Stdlib Require Export Sets.Image.
-From Stdlib Require Export Sets.Infinite_sets.
-From Stdlib Require Export Sets.Integers.
-From Stdlib Require Export Sets.Multiset.
-From Stdlib Require Export Sets.Partial_Order.
-From Stdlib Require Export Sets.Permut.
-From Stdlib Require Export Sets.Powerset.
-From Stdlib Require Export Sets.Powerset_Classical_facts.
-From Stdlib Require Export Sets.Powerset_facts.
-From Stdlib Require Export Sets.Relations_1.
-From Stdlib Require Export Sets.Relations_1_facts.
-From Stdlib Require Export Sets.Relations_2.
-From Stdlib Require Export Sets.Relations_2_facts.
-From Stdlib Require Export Sets.Relations_3.
-From Stdlib Require Export Sets.Relations_3_facts.
-From Stdlib Require Export Sets.Uniset.
-From Stdlib Require Export Setoids.Setoid.
-From Stdlib Require Export Relations.Operators_Properties.
-From Stdlib Require Export Relations.Relation_Definitions.
-From Stdlib Require Export Relations.Relation_Operators.
-From Stdlib Require Export Relations.Relations.
-From Stdlib Require Export Reals.Alembert.
-From Stdlib Require Export Reals.AltSeries.
-From Stdlib Require Export Reals.ArithProp.
-From Stdlib Require Export Reals.Binomial.
-From Stdlib Require Export Reals.Cauchy_prod.
-From Stdlib Require Export Reals.ClassicalConstructiveReals.
-From Stdlib Require Export Reals.ClassicalDedekindReals.
-From Stdlib Require Export Reals.Cos_plus.
-From Stdlib Require Export Reals.Cos_rel.
-From Stdlib Require Export Reals.DiscrR.
-From Stdlib Require Export Reals.Exp_prop.
-From Stdlib Require Export Reals.Integration.
-From Stdlib Require Export Reals.MVT.
-From Stdlib Require Export Reals.Machin.
-From Stdlib Require Export Reals.NewtonInt.
-From Stdlib Require Export Reals.Nsatz.
-From Stdlib Require Export Reals.RNsatz.
-From Stdlib Require Export QArith.QNsatz.
-From Stdlib Require Export ZArith.ZNsatz.
-From Stdlib Require Export Reals.PSeries_reg.
-From Stdlib Require Export Reals.PartSum.
-From Stdlib Require Export Reals.Qreals.
-From Stdlib Require Export Reals.RIneq.
-From Stdlib Require Export Reals.RList.
-From Stdlib Require Export Reals.ROrderedType.
-From Stdlib Require Export Reals.R_Ifp.
-From Stdlib Require Export Reals.R_sqr.
-From Stdlib Require Export Reals.R_sqrt.
-From Stdlib Require Export Reals.Ranalysis.
-From Stdlib Require Export Reals.Ranalysis1.
-From Stdlib Require Export Reals.Ranalysis2.
-From Stdlib Require Export Reals.Ranalysis3.
-From Stdlib Require Export Reals.Ranalysis4.
-From Stdlib Require Export Reals.Ranalysis5.
-From Stdlib Require Export Reals.Ranalysis_reg.
-From Stdlib Require Export Reals.Ratan.
-From Stdlib Require Export Reals.Raxioms.
-From Stdlib Require Export Reals.Rbase.
-From Stdlib Require Export Reals.Rbasic_fun.
-From Stdlib Require Export Reals.Rcomplete.
-From Stdlib Require Export Reals.Rdefinitions.
-From Stdlib Require Export Reals.Rderiv.
-From Stdlib Require Export Reals.Reals.
-From Stdlib Require Export Reals.Rfunctions.
-From Stdlib Require Export Reals.Rgeom.
-From Stdlib Require Export Reals.RiemannInt.
-From Stdlib Require Export Reals.RiemannInt_SF.
-From Stdlib Require Export Reals.Rlimit.
-From Stdlib Require Export Reals.Rlogic.
-From Stdlib Require Export Reals.Rminmax.
-From Stdlib Require Export Reals.Rpow_def.
-From Stdlib Require Export Reals.Rpower.
-From Stdlib Require Export Reals.Rprod.
-From Stdlib Require Export Reals.Rregisternames.
-From Stdlib Require Export Reals.Rseries.
-From Stdlib Require Export Reals.Rsigma.
-From Stdlib Require Export Reals.Rsqrt_def.
-From Stdlib Require Export Reals.Rtopology.
-From Stdlib Require Export Reals.Rtrigo.
-From Stdlib Require Export Reals.Rtrigo1.
-From Stdlib Require Export Reals.Rtrigo_alt.
-From Stdlib Require Export Reals.Rtrigo_calc.
-From Stdlib Require Export Reals.Rtrigo_def.
-From Stdlib Require Export Reals.Rtrigo_facts.
-From Stdlib Require Export Reals.Rtrigo_fun.
-From Stdlib Require Export Reals.Rtrigo_reg.
-From Stdlib Require Export Reals.Runcountable.
-From Stdlib Require Export Reals.SeqProp.
-From Stdlib Require Export Reals.SeqSeries.
-From Stdlib Require Export Reals.SplitAbsolu.
-From Stdlib Require Export Reals.SplitRmult.
-From Stdlib Require Export Reals.Sqrt_reg.
-From Stdlib Require Export Reals.Zfloor.
-From Stdlib Require Export Reals.Cauchy.ConstructiveCauchyAbs.
-From Stdlib Require Export Reals.Cauchy.ConstructiveCauchyReals.
-From Stdlib Require Export Reals.Cauchy.ConstructiveCauchyRealsMult.
-From Stdlib Require Export Reals.Cauchy.ConstructiveExtra.
-From Stdlib Require Export Reals.Cauchy.ConstructiveRcomplete.
-From Stdlib Require Export Reals.Cauchy.PosExtra.
-From Stdlib Require Export Reals.Cauchy.QExtra.
-From Stdlib Require Export Reals.Abstract.ConstructiveAbs.
-From Stdlib Require Export Reals.Abstract.ConstructiveLUB.
-From Stdlib Require Export Reals.Abstract.ConstructiveLimits.
-From Stdlib Require Export Reals.Abstract.ConstructiveMinMax.
-From Stdlib Require Export Reals.Abstract.ConstructivePower.
-From Stdlib Require Export Reals.Abstract.ConstructiveReals.
-From Stdlib Require Export Reals.Abstract.ConstructiveRealsMorphisms.
-From Stdlib Require Export Reals.Abstract.ConstructiveSum.
-From Stdlib Require Export QArith.QArith.
-From Stdlib Require Export QArith.QArith_base.
-From Stdlib Require Export QArith.QOrderedType.
-From Stdlib Require Export QArith.Qabs.
-From Stdlib Require Export QArith.Qcabs.
-From Stdlib Require Export QArith.Qcanon.
-From Stdlib Require Export QArith.Qfield.
-From Stdlib Require Export QArith.Qminmax.
-From Stdlib Require Export QArith.Qpower.
-From Stdlib Require Export QArith.Qreduction.
-From Stdlib Require Export QArith.Qring.
-From Stdlib Require Export QArith.Qround.
-From Stdlib Require Export Program.Basics.
-From Stdlib Require Export Program.Combinators.
-From Stdlib Require Export Program.Equality.
-From Stdlib Require Export Program.Program.
-From Stdlib Require Export Program.Subset.
-From Stdlib Require Export Program.Syntax.
-From Stdlib Require Export Program.Tactics.
-From Stdlib Require Export Program.Utils.
-From Stdlib Require Export Program.Wf.
-From Stdlib Require Export Program.WfExtensionality.
-From Stdlib Require Export PArith.BinPos.
-From Stdlib Require Export PArith.BinPosDef.
-From Stdlib Require Export PArith.PArith.
-From Stdlib Require Export PArith.POrderedType.
-From Stdlib Require Export PArith.Pnat.
-From Stdlib Require Export Numbers.AltBinNotations.
-From Stdlib Require Export Numbers.BinNums.
-From Stdlib Require Export Numbers.DecimalFacts.
-From Stdlib Require Export Numbers.DecimalN.
-From Stdlib Require Export Numbers.DecimalNat.
-From Stdlib Require Export Numbers.DecimalPos.
-From Stdlib Require Export Numbers.DecimalQ.
-From Stdlib Require Export Numbers.DecimalR.
-From Stdlib Require Export Numbers.DecimalString.
-From Stdlib Require Export Numbers.DecimalZ.
-From Stdlib Require Export Numbers.HexadecimalFacts.
-From Stdlib Require Export Numbers.HexadecimalN.
-From Stdlib Require Export Numbers.HexadecimalNat.
-From Stdlib Require Export Numbers.HexadecimalPos.
-From Stdlib Require Export Numbers.HexadecimalQ.
-From Stdlib Require Export Numbers.HexadecimalR.
-From Stdlib Require Export Numbers.HexadecimalString.
-From Stdlib Require Export Numbers.HexadecimalZ.
-From Stdlib Require Export Numbers.NaryFunctions.
-From Stdlib Require Export Numbers.NumPrelude.
-From Stdlib Require Export Numbers.Natural.Binary.NBinary.
-From Stdlib Require Export Numbers.Natural.Abstract.NAdd.
-From Stdlib Require Export Numbers.Natural.Abstract.NAddOrder.
-From Stdlib Require Export Numbers.Natural.Abstract.NAxioms.
-From Stdlib Require Export Numbers.Natural.Abstract.NBase.
-From Stdlib Require Export Numbers.Natural.Abstract.NBits.
-From Stdlib Require Export Numbers.Natural.Abstract.NDefOps.
-From Stdlib Require Export Numbers.Natural.Abstract.NDiv.
-From Stdlib Require Export Numbers.Natural.Abstract.NDiv0.
-From Stdlib Require Export Numbers.Natural.Abstract.NGcd.
-From Stdlib Require Export Numbers.Natural.Abstract.NIso.
-From Stdlib Require Export Numbers.Natural.Abstract.NLcm.
-From Stdlib Require Export Numbers.Natural.Abstract.NLcm0.
-From Stdlib Require Export Numbers.Natural.Abstract.NLog.
-From Stdlib Require Export Numbers.Natural.Abstract.NMaxMin.
-From Stdlib Require Export Numbers.Natural.Abstract.NMulOrder.
-From Stdlib Require Export Numbers.Natural.Abstract.NOrder.
-From Stdlib Require Export Numbers.Natural.Abstract.NParity.
-From Stdlib Require Export Numbers.Natural.Abstract.NPow.
-From Stdlib Require Export Numbers.Natural.Abstract.NProperties.
-From Stdlib Require Export Numbers.Natural.Abstract.NSqrt.
-From Stdlib Require Export Numbers.Natural.Abstract.NStrongRec.
-From Stdlib Require Export Numbers.Natural.Abstract.NSub.
-From Stdlib Require Export Numbers.NatInt.NZAdd.
-From Stdlib Require Export Numbers.NatInt.NZAddOrder.
-From Stdlib Require Export Numbers.NatInt.NZAxioms.
-From Stdlib Require Export Numbers.NatInt.NZBase.
-From Stdlib Require Export Numbers.NatInt.NZBits.
-From Stdlib Require Export Numbers.NatInt.NZDiv.
-From Stdlib Require Export Numbers.NatInt.NZDomain.
-From Stdlib Require Export Numbers.NatInt.NZGcd.
-From Stdlib Require Export Numbers.NatInt.NZLog.
-From Stdlib Require Export Numbers.NatInt.NZMul.
-From Stdlib Require Export Numbers.NatInt.NZMulOrder.
-From Stdlib Require Export Numbers.NatInt.NZOrder.
-From Stdlib Require Export Numbers.NatInt.NZParity.
-From Stdlib Require Export Numbers.NatInt.NZPow.
-From Stdlib Require Export Numbers.NatInt.NZProperties.
-From Stdlib Require Export Numbers.NatInt.NZSqrt.
-From Stdlib Require Export Numbers.Integer.NatPairs.ZNatPairs.
-From Stdlib Require Export Numbers.Integer.Binary.ZBinary.
-From Stdlib Require Export Numbers.Integer.Abstract.ZAdd.
-From Stdlib Require Export Numbers.Integer.Abstract.ZAddOrder.
-From Stdlib Require Export Numbers.Integer.Abstract.ZAxioms.
-From Stdlib Require Export Numbers.Integer.Abstract.ZBase.
-From Stdlib Require Export Numbers.Integer.Abstract.ZBits.
-From Stdlib Require Export Numbers.Integer.Abstract.ZDivEucl.
-From Stdlib Require Export Numbers.Integer.Abstract.ZDivFloor.
-From Stdlib Require Export Numbers.Integer.Abstract.ZDivTrunc.
-From Stdlib Require Export Numbers.Integer.Abstract.ZGcd.
-From Stdlib Require Export Numbers.Integer.Abstract.ZLcm.
-From Stdlib Require Export Numbers.Integer.Abstract.ZLt.
-From Stdlib Require Export Numbers.Integer.Abstract.ZMaxMin.
-From Stdlib Require Export Numbers.Integer.Abstract.ZMul.
-From Stdlib Require Export Numbers.Integer.Abstract.ZMulOrder.
-From Stdlib Require Export Numbers.Integer.Abstract.ZParity.
-From Stdlib Require Export Numbers.Integer.Abstract.ZPow.
-From Stdlib Require Export Numbers.Integer.Abstract.ZProperties.
-From Stdlib Require Export Numbers.Integer.Abstract.ZSgnAbs.
-From Stdlib Require Export Numbers.Cyclic.Int63.CarryType.
-From Stdlib Require Export Numbers.Cyclic.Int63.Cyclic63.
-From Stdlib Require Export Numbers.Cyclic.Int63.PrimInt63.
-From Stdlib Require Export Numbers.Cyclic.Int63.Ring63.
-From Stdlib Require Export Numbers.Cyclic.Int63.Sint63.
-From Stdlib Require Export Numbers.Cyclic.Int63.Sint63Axioms.
-From Stdlib Require Export Numbers.Cyclic.Int63.Uint63.
-From Stdlib Require Export Numbers.Cyclic.Int63.Uint63Axioms.
-From Stdlib Require Export Numbers.Cyclic.Abstract.CyclicAxioms.
-From Stdlib Require Export Numbers.Cyclic.Abstract.DoubleType.
-From Stdlib Require Export Numbers.Cyclic.Abstract.NZCyclic.
-From Stdlib Require Export NArith.BinNat.
-From Stdlib Require Export NArith.BinNatDef.
-From Stdlib Require Export NArith.NArith.
-From Stdlib Require Export NArith.NArith_base.
-From Stdlib Require Export NArith.Ndec.
-From Stdlib Require Export NArith.Ndiv_def.
-From Stdlib Require Export NArith.Ngcd_def.
-From Stdlib Require Export NArith.Nnat.
-From Stdlib Require Export NArith.Nsqrt_def.
-From Stdlib Require Export MSets.MSetAVL.
-From Stdlib Require Export MSets.MSetDecide.
-From Stdlib Require Export MSets.MSetEqProperties.
-From Stdlib Require Export MSets.MSetFacts.
-From Stdlib Require Export MSets.MSetGenTree.
-From Stdlib Require Export MSets.MSetInterface.
-From Stdlib Require Export MSets.MSetList.
-From Stdlib Require Export MSets.MSetPositive.
-From Stdlib Require Export MSets.MSetProperties.
-From Stdlib Require Export MSets.MSetRBT.
-From Stdlib Require Export MSets.MSetToFiniteSet.
-From Stdlib Require Export MSets.MSetWeakList.
-From Stdlib Require Export MSets.MSets.
-From Stdlib Require Export Logic.Adjointification.
-From Stdlib Require Export Logic.Berardi.
-From Stdlib Require Export Logic.ChoiceFacts.
-From Stdlib Require Export Logic.Classical.
-From Stdlib Require Export Logic.ClassicalChoice.
-From Stdlib Require Export Logic.ClassicalDescription.
-From Stdlib Require Export Logic.ClassicalEpsilon.
-From Stdlib Require Export Logic.ClassicalFacts.
-From Stdlib Require Export Logic.ClassicalUniqueChoice.
-From Stdlib Require Export Logic.Classical_Pred_Type.
-From Stdlib Require Export Logic.Classical_Prop.
-From Stdlib Require Export Logic.ConstructiveEpsilon.
-From Stdlib Require Export Logic.Decidable.
-From Stdlib Require Export Logic.Description.
-From Stdlib Require Export Logic.Diaconescu.
-From Stdlib Require Export Logic.Epsilon.
-From Stdlib Require Export Logic.Eqdep.
-From Stdlib Require Export Logic.EqdepFacts.
-From Stdlib Require Export Logic.Eqdep_dec.
-From Stdlib Require Export Logic.ExtensionalFunctionRepresentative.
-From Stdlib Require Export Logic.ExtensionalityFacts.
-From Stdlib Require Export Logic.FunctionalExtensionality.
-From Stdlib Require Export Logic.HLevelsBase.
-From Stdlib Require Export Logic.HLevels.
-From Stdlib Require Export Logic.Hurkens.
-From Stdlib Require Export Logic.IndefiniteDescription.
-From Stdlib Require Export Logic.JMeq.
-From Stdlib Require Export Logic.ProofIrrelevance.
-From Stdlib Require Export Logic.ProofIrrelevanceFacts.
-From Stdlib Require Export Logic.PropExtensionality.
-From Stdlib Require Export Logic.PropExtensionalityFacts.
-From Stdlib Require Export Logic.PropFacts.
-From Stdlib Require Export Logic.RelationalChoice.
-From Stdlib Require Export Logic.SetIsType.
-From Stdlib Require Export Logic.SetoidChoice.
-From Stdlib Require Export Logic.StrictProp.
-From Stdlib Require Export Logic.WKL.
-From Stdlib Require Export Logic.WeakFan.
-From Stdlib Require Export Lists.List.
-From Stdlib Require Export Lists.ListDec.
-From Stdlib Require Export Lists.ListDef.
-From Stdlib Require Export Lists.ListSet.
-From Stdlib Require Export Lists.ListTactics.
-From Stdlib Require Export Init.Byte.
-From Stdlib Require Export Init.Datatypes.
-From Stdlib Require Export Init.Decimal.
-From Stdlib Require Export Init.Hexadecimal.
-From Stdlib Require Export Init.Logic.
-From Stdlib Require Export Init.Ltac.
-From Stdlib Require Export Init.Nat.
-From Stdlib Require Export Init.Notations.
-From Stdlib Require Export Init.Number.
-From Stdlib Require Export Init.Peano.
-From Stdlib Require Export Init.Prelude.
-From Stdlib Require Export Init.Specif.
-From Stdlib Require Export Init.Sumbool.
-From Stdlib Require Export Init.Tactics.
-From Stdlib Require Export Init.Tauto.
-From Stdlib Require Export Init.Wf.
-From Stdlib Require Export Floats.FloatAxioms.
-From Stdlib Require Export Floats.FloatClass.
-From Stdlib Require Export Floats.FloatLemmas.
-From Stdlib Require Export Floats.FloatOps.
-From Stdlib Require Export Floats.Floats.
-From Stdlib Require Export Floats.PrimFloat.
-From Stdlib Require Export Floats.SpecFloat.
-From Stdlib Require Export FSets.FMapAVL.
-From Stdlib Require Export FSets.FMapFacts.
-From Stdlib Require Export FSets.FMapFullAVL.
-From Stdlib Require Export FSets.FMapInterface.
-From Stdlib Require Export FSets.FMapList.
-From Stdlib Require Export FSets.FMapPositive.
-From Stdlib Require Export FSets.FMapWeakList.
-From Stdlib Require Export FSets.FMaps.
-From Stdlib Require Export FSets.FSetAVL.
-From Stdlib Require Export FSets.FSetBridge.
-From Stdlib Require Export FSets.FSetCompat.
-From Stdlib Require Export FSets.FSetDecide.
-From Stdlib Require Export FSets.FSetEqProperties.
-From Stdlib Require Export FSets.FSetFacts.
-From Stdlib Require Export FSets.FSetInterface.
-From Stdlib Require Export FSets.FSetList.
-From Stdlib Require Export FSets.FSetPositive.
-From Stdlib Require Export FSets.FSetProperties.
-From Stdlib Require Export FSets.FSetToFiniteSet.
-From Stdlib Require Export FSets.FSetWeakList.
-From Stdlib Require Export FSets.FSets.
-From Stdlib Require Export Compat.AdmitAxiom.
-From Stdlib Require Export Compat.Coq818.
-From Stdlib Require Export Compat.Coq819.
-From Stdlib Require Export Compat.Coq820.
-From Stdlib Require Export Compat.Stdlib818.
-From Stdlib Require Export Classes.CEquivalence.
-From Stdlib Require Export Classes.CMorphisms.
-From Stdlib Require Export Classes.CRelationClasses.
-From Stdlib Require Export Classes.DecidableClass.
-From Stdlib Require Export Classes.EquivDec.
-From Stdlib Require Export Classes.Equivalence.
-From Stdlib Require Export Classes.Init.
-From Stdlib Require Export Classes.Morphisms.
-From Stdlib Require Export Classes.Morphisms_Prop.
-From Stdlib Require Export Classes.Morphisms_Relations.
-From Stdlib Require Export Classes.RelationClasses.
-From Stdlib Require Export Classes.RelationPairs.
-From Stdlib Require Export Classes.SetoidClass.
-From Stdlib Require Export Classes.SetoidDec.
-From Stdlib Require Export Classes.SetoidTactics.
-From Stdlib Require Export Bool.Bool.
-From Stdlib Require Export Bool.BoolEq.
-From Stdlib Require Export Bool.DecBool.
-From Stdlib Require Export Bool.IfProp.
-From Stdlib Require Export BinNums.IntDef.
-From Stdlib Require Export BinNums.NatDef.
-From Stdlib Require Export BinNums.PosDef.
-From Stdlib Require Export Array.ArrayAxioms.
-From Stdlib Require Export Array.PArray.
-From Stdlib Require Export Array.PrimArray.
-From Stdlib Require Export Arith.Arith.
-From Stdlib Require Export Arith.Arith_base.
-From Stdlib Require Export Arith.Between.
-From Stdlib Require Export Arith.Bool_nat.
-From Stdlib Require Export Arith.Cantor.
-From Stdlib Require Export Arith.Compare.
-From Stdlib Require Export Arith.Compare_dec.
-From Stdlib Require Export Arith.EqNat.
-From Stdlib Require Export Arith.Euclid.
-From Stdlib Require Export Arith.Factorial.
-From Stdlib Require Export Arith.PeanoNat.
-From Stdlib Require Export Arith.Peano_dec.
-From Stdlib Require Export Arith.Wf_nat.
-From Stdlib Require Export Arith.Zerob.
-From Stdlib Require Export Zmod.Zmod.
-From Stdlib Require Export Zmod.ZmodDef.
-From Stdlib Require Export Zmod.ZmodBase.
-From Stdlib Require Export Zmod.ZmodInv.
-From Stdlib Require Export Zmod.Zstar.
-From Stdlib Require Export Zmod.ZstarDef.
-From Stdlib Require Export Zmod.ZstarBase.
-From Stdlib Require Export Zmod.Bits.
diff --git a/theories/Make.all b/theories/Make.all
deleted file mode 100644
index d2bb5badca..0000000000
--- a/theories/Make.all
+++ /dev/null
@@ -1,3 +0,0 @@
-All/All.v
-
--Q All Stdlib.All
diff --git a/theories/Make.arith b/theories/Make.arith
deleted file mode 100644
index 7fbe1f1a3a..0000000000
--- a/theories/Make.arith
+++ /dev/null
@@ -1,3 +0,0 @@
-Arith/_All/Arith.v
-
--Q Arith/_All Stdlib.Arith
diff --git a/theories/Make.arith-base b/theories/Make.arith-base
deleted file mode 100644
index a3fec9a734..0000000000
--- a/theories/Make.arith-base
+++ /dev/null
@@ -1,59 +0,0 @@
-Arith/_Base/Arith_base.v
-Arith/_Base/Between.v
-Arith/_Base/Bool_nat.v
-Arith/_Base/Cantor.v
-Arith/_Base/Compare.v
-Arith/_Base/Compare_dec.v
-Arith/_Base/EqNat.v
-Arith/_Base/Euclid.v
-Arith/_Base/Factorial.v
-Arith/_Base/PeanoNat.v
-Arith/_Base/Peano_dec.v
-Arith/_Base/Wf_nat.v
-Arith/_Base/Zerob.v
-Numbers/_Arith/NumPrelude.v
-Numbers/NatInt/NZBase.v
-Numbers/NatInt/NZOrder.v
-Numbers/NatInt/NZProperties.v
-Numbers/NatInt/NZDiv.v
-Numbers/NatInt/NZParity.v
-Numbers/NatInt/NZPow.v
-Numbers/NatInt/NZSqrt.v
-Numbers/NatInt/NZGcd.v
-Numbers/NatInt/NZBits.v
-Numbers/NatInt/NZDomain.v
-Numbers/NatInt/NZAxioms.v
-Numbers/NatInt/NZAddOrder.v
-Numbers/NatInt/NZMul.v
-Numbers/NatInt/NZLog.v
-Numbers/NatInt/NZAdd.v
-Numbers/NatInt/NZMulOrder.v
-Numbers/Natural/Abstract/NStrongRec.v
-Numbers/Natural/Abstract/NAdd.v
-Numbers/Natural/Abstract/NAxioms.v
-Numbers/Natural/Abstract/NDefOps.v
-Numbers/Natural/Abstract/NSqrt.v
-Numbers/Natural/Abstract/NDiv0.v
-Numbers/Natural/Abstract/NBits.v
-Numbers/Natural/Abstract/NGcd.v
-Numbers/Natural/Abstract/NParity.v
-Numbers/Natural/Abstract/NProperties.v
-Numbers/Natural/Abstract/NMaxMin.v
-Numbers/Natural/Abstract/NDiv.v
-Numbers/Natural/Abstract/NPow.v
-Numbers/Natural/Abstract/NAddOrder.v
-Numbers/Natural/Abstract/NLcm0.v
-Numbers/Natural/Abstract/NLog.v
-Numbers/Natural/Abstract/NMulOrder.v
-Numbers/Natural/Abstract/NIso.v
-Numbers/Natural/Abstract/NSub.v
-Numbers/Natural/Abstract/NBase.v
-Numbers/Natural/Abstract/NLcm.v
-Numbers/Natural/Abstract/NOrder.v
-Classes/_Arith/SetoidDec.v
-
--Q Arith/_Base Stdlib.Arith
--Q Numbers/NatInt Stdlib.Numbers.NatInt
--Q Numbers/Natural Stdlib.Numbers.Natural
--Q Numbers/_Arith Stdlib.Numbers
--Q Classes/_Arith Stdlib.Classes
diff --git a/theories/Make.bool b/theories/Make.bool
deleted file mode 100644
index 05b73a20cd..0000000000
--- a/theories/Make.bool
+++ /dev/null
@@ -1,6 +0,0 @@
-Bool/IfProp.v
-Bool/Bool.v
-Bool/DecBool.v
-Bool/BoolEq.v
-
--Q Bool Stdlib.Bool
diff --git a/theories/Make.classes b/theories/Make.classes
deleted file mode 100644
index 746ff24be9..0000000000
--- a/theories/Make.classes
+++ /dev/null
@@ -1,7 +0,0 @@
-Classes/_All/CEquivalence.v
-Classes/_All/DecidableClass.v
-Classes/_All/Morphisms_Relations.v
-Classes/_All/RelationPairs.v
-Classes/_All/SetoidClass.v
-
--Q Classes/_All Stdlib.Classes
diff --git a/theories/Make.classical-logic b/theories/Make.classical-logic
deleted file mode 100644
index 05e5e90172..0000000000
--- a/theories/Make.classical-logic
+++ /dev/null
@@ -1,17 +0,0 @@
-Logic/_Classical/IndefiniteDescription.v
-Logic/_Classical/Classical_Pred_Type.v
-Logic/_Classical/Classical_Prop.v
-Logic/_Classical/ClassicalFacts.v
-Logic/_Classical/Classical.v
-Logic/_Classical/Epsilon.v
-Logic/_Classical/ClassicalChoice.v
-Logic/_Classical/Description.v
-Logic/_Classical/ClassicalEpsilon.v
-Logic/_Classical/ChoiceFacts.v
-Logic/_Classical/PropExtensionality.v
-Logic/_Classical/ClassicalDescription.v
-Logic/_Classical/ClassicalUniqueChoice.v
-Logic/_Classical/SetoidChoice.v
-Logic/_Classical/Diaconescu.v
-
--Q Logic/_Classical Stdlib.Logic
diff --git a/theories/Make.compat b/theories/Make.compat
deleted file mode 100644
index ec446b2501..0000000000
--- a/theories/Make.compat
+++ /dev/null
@@ -1,6 +0,0 @@
-Compat/_All/AdmitAxiom.v
-Compat/_All/Stdlib818.v
-Reals/_Compat/Nsatz.v
-
--Q Reals/_Compat Stdlib.Reals
--Q Compat/_All Stdlib.Compat
diff --git a/theories/Make.corelib-wrapper b/theories/Make.corelib-wrapper
deleted file mode 100644
index 59c579b9cd..0000000000
--- a/theories/Make.corelib-wrapper
+++ /dev/null
@@ -1,80 +0,0 @@
-Array/_CorelibWrapper/ArrayAxioms.v
-Array/_CorelibWrapper/PrimArray.v
-BinNums/_CorelibWrapper/IntDef.v
-BinNums/_CorelibWrapper/NatDef.v
-BinNums/_CorelibWrapper/PosDef.v
-Classes/_CorelibWrapper/CMorphisms.v
-Classes/_CorelibWrapper/CRelationClasses.v
-Classes/_CorelibWrapper/Equivalence.v
-Classes/_CorelibWrapper/Init.v
-Classes/_CorelibWrapper/Morphisms.v
-Classes/_CorelibWrapper/Morphisms_Prop.v
-Classes/_CorelibWrapper/RelationClasses.v
-Classes/_CorelibWrapper/SetoidTactics.v
-Compat/_CorelibWrapper/Coq818.v
-Compat/_CorelibWrapper/Coq819.v
-Compat/_CorelibWrapper/Coq820.v
-Floats/_CorelibWrapper/FloatAxioms.v
-Floats/_CorelibWrapper/FloatClass.v
-Floats/_CorelibWrapper/FloatOps.v
-Floats/_CorelibWrapper/PrimFloat.v
-Floats/_CorelibWrapper/SpecFloat.v
-Init/_CorelibWrapper/Byte.v
-Init/_CorelibWrapper/Datatypes.v
-Init/_CorelibWrapper/Decimal.v
-Init/_CorelibWrapper/Hexadecimal.v
-Init/_CorelibWrapper/Logic.v
-Init/_CorelibWrapper/Ltac.v
-Init/_CorelibWrapper/Nat.v
-Init/_CorelibWrapper/Notations.v
-Init/_CorelibWrapper/Number.v
-Init/_CorelibWrapper/Peano.v
-Init/_CorelibWrapper/Prelude.v
-Init/_CorelibWrapper/Specif.v
-Init/_CorelibWrapper/Sumbool.v
-Init/_CorelibWrapper/Tactics.v
-Init/_CorelibWrapper/Tauto.v
-Init/_CorelibWrapper/Wf.v
-Lists/_CorelibWrapper/ListDef.v
-Numbers/_CorelibWrapper/BinNums.v
-Numbers/Cyclic/Int63/_CorelibWrapper/CarryType.v
-Numbers/Cyclic/Int63/_CorelibWrapper/PrimInt63.v
-Numbers/Cyclic/Int63/_CorelibWrapper/Sint63Axioms.v
-Numbers/Cyclic/Int63/_CorelibWrapper/Uint63Axioms.v
-Program/_CorelibWrapper/Basics.v
-Program/_CorelibWrapper/Tactics.v
-Program/_CorelibWrapper/Utils.v
-Program/_CorelibWrapper/Wf.v
-Relations/_CorelibWrapper/Relation_Definitions.v
-Setoids/Setoid.v
-Strings/_CorelibWrapper/PrimString.v
-Strings/_CorelibWrapper/PrimStringAxioms.v
-derive/Derive.v
-extraction/_CorelibWrapper/ExtrHaskellBasic.v
-extraction/_CorelibWrapper/ExtrOcamlBasic.v
-extraction/_CorelibWrapper/Extraction.v
-ssr/ssrbool.v
-ssr/ssrclasses.v
-ssr/ssreflect.v
-ssr/ssrfun.v
-ssr/ssrsetoid.v
-ssr/ssrunder.v
-ssrmatching/ssrmatching.v
-
--Q Array/_CorelibWrapper Stdlib.Array
--Q BinNums/_CorelibWrapper Stdlib.BinNums
--Q Classes/_CorelibWrapper Stdlib.Classes
--Q Compat/_CorelibWrapper Stdlib.Compat
--Q Floats/_CorelibWrapper Stdlib.Floats
--Q Init/_CorelibWrapper Stdlib.Init
--Q Lists/_CorelibWrapper Stdlib.Lists
--Q Numbers/_CorelibWrapper Stdlib.Numbers
--Q Numbers/Cyclic/Int63/_CorelibWrapper Stdlib.Numbers.Cyclic.Int63
--Q Program/_CorelibWrapper Stdlib.Program
--Q Relations/_CorelibWrapper Stdlib.Relations
--Q Setoids Stdlib.Setoids
--Q Strings/_CorelibWrapper Stdlib.Strings
--Q derive Stdlib.derive
--Q extraction/_CorelibWrapper Stdlib.extraction
--Q ssr Stdlib.ssr
--Q ssrmatching Stdlib.ssrmatching
diff --git a/theories/Make.extraction b/theories/Make.extraction
deleted file mode 100644
index 274242c6b2..0000000000
--- a/theories/Make.extraction
+++ /dev/null
@@ -1,21 +0,0 @@
-extraction/_All/ExtrHaskellZInteger.v
-extraction/_All/ExtrHaskellZInt.v
-extraction/_All/ExtrHaskellNatNum.v
-extraction/_All/ExtrHaskellString.v
-extraction/_All/ExtrOcamlZInt.v
-extraction/_All/ExtrOcamlNativeString.v
-extraction/_All/ExtrOCamlFloats.v
-extraction/_All/ExtrOcamlNatBigInt.v
-extraction/_All/ExtrOcamlZBigInt.v
-extraction/_All/ExtrOcamlNatInt.v
-extraction/_All/ExtrHaskellNatInt.v
-extraction/_All/ExtrOcamlString.v
-extraction/_All/ExtrOCamlPString.v
-extraction/_All/ExtrHaskellZNum.v
-extraction/_All/ExtrOcamlChar.v
-extraction/_All/ExtrOCamlPArray.v
-extraction/_All/ExtrOcamlIntConv.v
-extraction/_All/ExtrOCamlInt63.v
-extraction/_All/ExtrHaskellNatInteger.v
-
--Q extraction/_All Stdlib.extraction
diff --git a/theories/Make.field b/theories/Make.field
deleted file mode 100644
index f912f144f4..0000000000
--- a/theories/Make.field
+++ /dev/null
@@ -1,5 +0,0 @@
-setoid_ring/_Field/Field_theory.v
-setoid_ring/_Field/Field_tac.v
-setoid_ring/_Field/Field.v
-
--Q setoid_ring/_Field Stdlib.setoid_ring
diff --git a/theories/Make.fmaps-fsets-msets b/theories/Make.fmaps-fsets-msets
deleted file mode 100644
index 3bb3bc1536..0000000000
--- a/theories/Make.fmaps-fsets-msets
+++ /dev/null
@@ -1,37 +0,0 @@
-FSets/FMapInterface.v
-FSets/FSetInterface.v
-FSets/FSetWeakList.v
-FSets/FSetAVL.v
-FSets/FSetCompat.v
-FSets/FSetDecide.v
-FSets/FSetList.v
-FSets/FSetProperties.v
-FSets/FMapList.v
-FSets/FMapFacts.v
-FSets/FSetPositive.v
-FSets/FMapFullAVL.v
-FSets/FSetToFiniteSet.v
-FSets/FMapAVL.v
-FSets/FMapPositive.v
-FSets/FSets.v
-FSets/FMaps.v
-FSets/FSetFacts.v
-FSets/FSetEqProperties.v
-FSets/FSetBridge.v
-FSets/FMapWeakList.v
-MSets/MSetList.v
-MSets/MSetDecide.v
-MSets/MSets.v
-MSets/MSetWeakList.v
-MSets/MSetGenTree.v
-MSets/MSetAVL.v
-MSets/MSetInterface.v
-MSets/MSetFacts.v
-MSets/MSetProperties.v
-MSets/MSetRBT.v
-MSets/MSetPositive.v
-MSets/MSetToFiniteSet.v
-MSets/MSetEqProperties.v
-
--Q FSets Stdlib.FSets
--Q MSets Stdlib.MSets
diff --git a/theories/Make.funind b/theories/Make.funind
deleted file mode 100644
index 9ad5d04e8d..0000000000
--- a/theories/Make.funind
+++ /dev/null
@@ -1,4 +0,0 @@
-funind/FunInd.v
-funind/Recdef.v
-
--Q funind Stdlib.funind
diff --git a/theories/Make.lia b/theories/Make.lia
deleted file mode 100644
index 5effe945ae..0000000000
--- a/theories/Make.lia
+++ /dev/null
@@ -1,26 +0,0 @@
-omega/OmegaLemmas.v
-omega/PreOmega.v
-micromega/_Lia/ZifyN.v
-micromega/_Lia/ZifyComparison.v
-micromega/_Lia/ZifyClasses.v
-micromega/_Lia/ZifyNat.v
-micromega/_Lia/ZifyPow.v
-micromega/_Lia/ZifyBool.v
-micromega/_Lia/Zify.v
-micromega/_Lia/ZifyInst.v
-micromega/_Lia/DeclConstantZ.v
-micromega/_Lia/OrderedRing.v
-micromega/_Lia/Tauto.v
-micromega/_Lia/Env.v
-micromega/_Lia/Refl.v
-micromega/_Lia/ZArith_hints.v
-micromega/_Lia/ZMicromega.v
-micromega/_Lia/EnvRing.v
-micromega/_Lia/Lia.v
-micromega/_Lia/VarMap.v
-micromega/_Lia/Ztac.v
-micromega/_Lia/ZCoeff.v
-micromega/_Lia/RingMicromega.v
-
--Q omega Stdlib.omega
--Q micromega/_Lia Stdlib.micromega
diff --git a/theories/Make.lists b/theories/Make.lists
deleted file mode 100644
index 44c26c02fd..0000000000
--- a/theories/Make.lists
+++ /dev/null
@@ -1,12 +0,0 @@
-Lists/_All/ListDec.v
-Lists/_All/List.v
-Lists/_All/ListSet.v
-Lists/_All/ListTactics.v
-Numbers/_Lists/NaryFunctions.v
-Logic/_Lists/WKL.v
-Classes/_Lists/EquivDec.v
-
--Q Lists/_All Stdlib.Lists
--Q Numbers/_Lists Stdlib.Numbers
--Q Logic/_Lists Stdlib.Logic
--Q Classes/_Lists Stdlib.Classes
diff --git a/theories/Make.logic b/theories/Make.logic
deleted file mode 100644
index 80fd121cfe..0000000000
--- a/theories/Make.logic
+++ /dev/null
@@ -1,24 +0,0 @@
-Logic/Adjointification.v
-Logic/Eqdep_dec.v
-Logic/JMeq.v
-Logic/SetIsType.v
-Logic/Berardi.v
-Logic/ExtensionalFunctionRepresentative.v
-Logic/ProofIrrelevanceFacts.v
-Logic/StrictProp.v
-Logic/ConstructiveEpsilon.v
-Logic/ExtensionalityFacts.v
-Logic/ProofIrrelevance.v
-Logic/WeakFan.v
-Logic/Decidable.v
-Logic/FunctionalExtensionality.v
-Logic/PropExtensionalityFacts.v
-Logic/Eqdep.v
-Logic/HLevelsBase.v
-Logic/HLevels.v
-Logic/PropFacts.v
-Logic/EqdepFacts.v
-Logic/Hurkens.v
-Logic/RelationalChoice.v
-
--Q Logic Stdlib.Logic
diff --git a/theories/Make.lqa b/theories/Make.lqa
deleted file mode 100644
index f058d2a138..0000000000
--- a/theories/Make.lqa
+++ /dev/null
@@ -1,10 +0,0 @@
-micromega/_Lqa/QMicromega.v
-micromega/_Lqa/Lqa.v
-micromega/_Lqa/DeclConstant.v
-QArith/_Lqa/Qfield.v
-QArith/_Lqa/Qring.v
-setoid_ring/_QArith/Rings_Q.v
-
--Q micromega/_Lqa Stdlib.micromega
--Q QArith/_Lqa Stdlib.QArith
--Q setoid_ring/_QArith Stdlib.setoid_ring
diff --git a/theories/Make.narith b/theories/Make.narith
deleted file mode 100644
index d57666b46c..0000000000
--- a/theories/Make.narith
+++ /dev/null
@@ -1,3 +0,0 @@
-NArith/_All/NArith.v
-
--Q NArith/_All Stdlib.NArith
diff --git a/theories/Make.narith-base b/theories/Make.narith-base
deleted file mode 100644
index 49e2b187cb..0000000000
--- a/theories/Make.narith-base
+++ /dev/null
@@ -1,10 +0,0 @@
-NArith/_Base/BinNatDef.v
-NArith/_Base/BinNat.v
-NArith/_Base/Nnat.v
-NArith/_Base/Ndiv_def.v
-NArith/_Base/Ndec.v
-NArith/_Base/Ngcd_def.v
-NArith/_Base/Nsqrt_def.v
-NArith/_Base/NArith_base.v
-
--Q NArith/_Base Stdlib.NArith
diff --git a/theories/Make.orders-ex b/theories/Make.orders-ex
deleted file mode 100644
index 0ee9ecbe54..0000000000
--- a/theories/Make.orders-ex
+++ /dev/null
@@ -1,12 +0,0 @@
-Structures/_Ex/BoolOrder.v
-Structures/_Ex/OrdersEx.v
-Structures/_Ex/OrdersLists.v
-Structures/_Ex/EqualitiesFacts.v
-Structures/_Ex/OrderedTypeAlt.v
-Structures/_Ex/OrderedType.v
-Structures/_Ex/DecidableType.v
-Structures/_Ex/OrderedTypeEx.v
-Structures/_Ex/OrdersAlt.v
-Structures/_Ex/DecidableTypeEx.v
-
--Q Structures/_Ex Stdlib.Structures
diff --git a/theories/Make.positive b/theories/Make.positive
deleted file mode 100644
index f0672e975c..0000000000
--- a/theories/Make.positive
+++ /dev/null
@@ -1,9 +0,0 @@
-Numbers/_positive/AltBinNotations.v
-PArith/Pnat.v
-PArith/POrderedType.v
-PArith/BinPos.v
-PArith/PArith.v
-PArith/BinPosDef.v
-
--Q Numbers/_positive Stdlib.Numbers
--Q PArith Stdlib.PArith
diff --git a/theories/Make.primitive-array b/theories/Make.primitive-array
deleted file mode 100644
index 63f0e7afd0..0000000000
--- a/theories/Make.primitive-array
+++ /dev/null
@@ -1,3 +0,0 @@
-Array/_All/PArray.v
-
--Q Array/_All Stdlib.Array
diff --git a/theories/Make.primitive-floats b/theories/Make.primitive-floats
deleted file mode 100644
index bfdf039807..0000000000
--- a/theories/Make.primitive-floats
+++ /dev/null
@@ -1,4 +0,0 @@
-Floats/_All/Floats.v
-Floats/_All/FloatLemmas.v
-
--Q Floats/_All Stdlib.Floats
diff --git a/theories/Make.primitive-int b/theories/Make.primitive-int
deleted file mode 100644
index a6c0ad4c2a..0000000000
--- a/theories/Make.primitive-int
+++ /dev/null
@@ -1,13 +0,0 @@
-Numbers/Cyclic/Int63/_All/Sint63.v
-Numbers/Cyclic/Int63/_All/Cyclic63.v
-Numbers/Cyclic/Int63/_All/Uint63.v
-Numbers/Cyclic/Int63/_All/Ring63.v
-Numbers/Cyclic/Abstract/NZCyclic.v
-Numbers/Cyclic/Abstract/DoubleType.v
-Numbers/Cyclic/Abstract/CyclicAxioms.v
-micromega/_Int63/ZifyUint63.v
-micromega/_Int63/ZifySint63.v
-
--Q Numbers/Cyclic/Int63/_All Stdlib.Numbers.Cyclic.Int63
--Q Numbers/Cyclic/Abstract Stdlib.Numbers.Cyclic.Abstract
--Q micromega/_Int63 Stdlib.micromega
diff --git a/theories/Make.primitive-string b/theories/Make.primitive-string
deleted file mode 100644
index 475084b500..0000000000
--- a/theories/Make.primitive-string
+++ /dev/null
@@ -1,3 +0,0 @@
-Strings/_PString/PString.v
-
--Q Strings/_PString Stdlib.Strings
diff --git a/theories/Make.program b/theories/Make.program
deleted file mode 100644
index b26a5bb508..0000000000
--- a/theories/Make.program
+++ /dev/null
@@ -1,8 +0,0 @@
-Program/_All/Syntax.v
-Program/_All/Equality.v
-Program/_All/Subset.v
-Program/_All/WfExtensionality.v
-Program/_All/Program.v
-Program/_All/Combinators.v
-
--Q Program/_All Stdlib.Program
diff --git a/theories/Make.qarith b/theories/Make.qarith
deleted file mode 100644
index 506e63cf4b..0000000000
--- a/theories/Make.qarith
+++ /dev/null
@@ -1,12 +0,0 @@
-QArith/_All/Qcabs.v
-QArith/_All/Qround.v
-QArith/_All/Qabs.v
-QArith/_All/QArith.v
-QArith/_All/Qpower.v
-QArith/_All/Qcanon.v
-QArith/_All/QNsatz.v
-Numbers/_QArith/DecimalQ.v
-Numbers/_QArith/HexadecimalQ.v
-
--Q QArith/_All Stdlib.QArith
--Q Numbers/_QArith Stdlib.Numbers
diff --git a/theories/Make.qarith-base b/theories/Make.qarith-base
deleted file mode 100644
index efa2bef75d..0000000000
--- a/theories/Make.qarith-base
+++ /dev/null
@@ -1,6 +0,0 @@
-QArith/_Base/Qreduction.v
-QArith/_Base/Qminmax.v
-QArith/_Base/QOrderedType.v
-QArith/_Base/QArith_base.v
-
--Q QArith/_Base Stdlib.QArith
diff --git a/theories/Make.reals b/theories/Make.reals
deleted file mode 100644
index 1f53c5d59e..0000000000
--- a/theories/Make.reals
+++ /dev/null
@@ -1,99 +0,0 @@
-Reals/Rtrigo_facts.v
-Reals/Ranalysis2.v
-Reals/Rbase.v
-Reals/Reals.v
-Reals/ArithProp.v
-Reals/Rgeom.v
-Reals/Exp_prop.v
-Reals/Rtrigo.v
-Reals/PartSum.v
-Reals/SplitRmult.v
-Reals/Rprod.v
-Reals/Rsqrt_def.v
-Reals/Ranalysis3.v
-Reals/PSeries_reg.v
-Reals/Rtrigo_calc.v
-Reals/Raxioms.v
-Reals/Ratan.v
-Reals/Cos_plus.v
-Reals/Rderiv.v
-Reals/R_sqrt.v
-Reals/R_sqr.v
-Reals/Integration.v
-Reals/Sqrt_reg.v
-Reals/RiemannInt.v
-Reals/Ranalysis_reg.v
-Reals/NewtonInt.v
-Reals/Rtrigo1.v
-Reals/Rtrigo_fun.v
-Reals/Ranalysis1.v
-Reals/Zfloor.v
-Reals/Abstract/ConstructiveLimits.v
-Reals/Abstract/ConstructiveRealsMorphisms.v
-Reals/Abstract/ConstructiveAbs.v
-Reals/Abstract/ConstructiveLUB.v
-Reals/Abstract/ConstructivePower.v
-Reals/Abstract/ConstructiveReals.v
-Reals/Abstract/ConstructiveSum.v
-Reals/Abstract/ConstructiveMinMax.v
-Reals/RList.v
-Reals/Rsigma.v
-Reals/Runcountable.v
-Reals/Rpower.v
-Reals/Rregisternames.v
-Reals/RiemannInt_SF.v
-Reals/Rbasic_fun.v
-Reals/ROrderedType.v
-Reals/SeqSeries.v
-Reals/RIneq.v
-Reals/DiscrR.v
-Reals/SplitAbsolu.v
-Reals/ClassicalDedekindReals.v
-Reals/Rtrigo_def.v
-Reals/R_Ifp.v
-Reals/Rtopology.v
-Reals/Rfunctions.v
-Reals/Rtrigo_alt.v
-Reals/ClassicalConstructiveReals.v
-Reals/Cos_rel.v
-Reals/Cauchy/ConstructiveRcomplete.v
-Reals/Cauchy/QExtra.v
-Reals/Cauchy/ConstructiveCauchyAbs.v
-Reals/Cauchy/PosExtra.v
-Reals/Cauchy/ConstructiveExtra.v
-Reals/Cauchy/ConstructiveCauchyReals.v
-Reals/Cauchy/ConstructiveCauchyRealsMult.v
-Reals/Machin.v
-Reals/Alembert.v
-Reals/Ranalysis.v
-Reals/MVT.v
-Reals/Rlimit.v
-Reals/Ranalysis4.v
-Reals/Rdefinitions.v
-Reals/Rcomplete.v
-Reals/Ranalysis5.v
-Reals/Binomial.v
-Reals/Cauchy_prod.v
-Reals/Rtrigo_reg.v
-Reals/Rseries.v
-Reals/AltSeries.v
-Reals/Rminmax.v
-Reals/Rpow_def.v
-Reals/Rlogic.v
-Reals/SeqProp.v
-Reals/Qreals.v
-Reals/RNsatz.v
-setoid_ring/_Reals/RealField.v
-setoid_ring/_Reals/Rings_R.v
-micromega/_Reals/Lra.v
-micromega/_Reals/Psatz.v
-micromega/_Reals/Fourier_util.v
-micromega/_Reals/Fourier.v
-micromega/_Reals/RMicromega.v
-Numbers/_Reals/DecimalR.v
-Numbers/_Reals/HexadecimalR.v
-
--Q Reals Stdlib.Reals
--Q setoid_ring/_Reals Stdlib.setoid_ring
--Q micromega/_Reals Stdlib.micromega
--Q Numbers/_Reals Stdlib.Numbers
diff --git a/theories/Make.relations b/theories/Make.relations
deleted file mode 100644
index a74f0af4c8..0000000000
--- a/theories/Make.relations
+++ /dev/null
@@ -1,5 +0,0 @@
-Relations/_All/Relation_Operators.v
-Relations/_All/Operators_Properties.v
-Relations/_All/Relations.v
-
--Q Relations/_All Stdlib.Relations
diff --git a/theories/Make.ring b/theories/Make.ring
deleted file mode 100644
index 5821fbb2c0..0000000000
--- a/theories/Make.ring
+++ /dev/null
@@ -1,26 +0,0 @@
-ZArith/_Ring/Zpow_def.v
-ZArith/_Ring/Zcomplements.v
-ZArith/_Ring/Zdiv.v
-setoid_ring/_Ring/Ncring_polynom.v
-setoid_ring/_Ring/Rings_Z.v
-setoid_ring/_Ring/Ncring_initial.v
-setoid_ring/_Ring/Ring_polynom.v
-setoid_ring/_Ring/ZArithRing.v
-setoid_ring/_Ring/Integral_domain.v
-setoid_ring/_Ring/Ring_base.v
-setoid_ring/_Ring/BinList.v
-setoid_ring/_Ring/Ncring.v
-setoid_ring/_Ring/Ring.v
-setoid_ring/_Ring/Algebra_syntax.v
-setoid_ring/_Ring/InitialRing.v
-setoid_ring/_Ring/Cring.v
-setoid_ring/_Ring/Ncring_tac.v
-setoid_ring/_Ring/Ring_tac.v
-setoid_ring/_Ring/ArithRing.v
-setoid_ring/_Ring/NArithRing.v
-setoid_ring/_Ring/Ring_theory.v
-nsatz/NsatzTactic.v
-
--Q ZArith/_Ring Stdlib.ZArith
--Q setoid_ring/_Ring Stdlib.setoid_ring
--Q nsatz Stdlib.nsatz
diff --git a/theories/Make.rtauto b/theories/Make.rtauto
deleted file mode 100644
index 8d9f4e96d4..0000000000
--- a/theories/Make.rtauto
+++ /dev/null
@@ -1,4 +0,0 @@
-rtauto/Bintree.v
-rtauto/Rtauto.v
-
--Q rtauto Stdlib.rtauto
diff --git a/theories/Make.sets b/theories/Make.sets
deleted file mode 100644
index 1766fc79b1..0000000000
--- a/theories/Make.sets
+++ /dev/null
@@ -1,24 +0,0 @@
-Sets/Partial_Order.v
-Sets/Multiset.v
-Sets/Uniset.v
-Sets/Relations_2.v
-Sets/Image.v
-Sets/Relations_3.v
-Sets/Relations_1.v
-Sets/Classical_sets.v
-Sets/Finite_sets.v
-Sets/Permut.v
-Sets/Integers.v
-Sets/Finite_sets_facts.v
-Sets/Powerset_facts.v
-Sets/Powerset.v
-Sets/Powerset_Classical_facts.v
-Sets/Ensembles.v
-Sets/Relations_1_facts.v
-Sets/Constructive_sets.v
-Sets/Infinite_sets.v
-Sets/Relations_2_facts.v
-Sets/Relations_3_facts.v
-Sets/Cpo.v
-
--Q Sets Stdlib.Sets
diff --git a/theories/Make.sorting b/theories/Make.sorting
deleted file mode 100644
index dd1d383381..0000000000
--- a/theories/Make.sorting
+++ /dev/null
@@ -1,12 +0,0 @@
-Sorting/Heap.v
-Sorting/CPermutation.v
-Sorting/Mergesort.v
-Sorting/PermutSetoid.v
-Sorting/PermutEq.v
-Sorting/Sorting.v
-Sorting/Permutation.v
-Sorting/Sorted.v
-Sorting/SetoidList.v
-Sorting/SetoidPermutation.v
-
--Q Sorting Stdlib.Sorting
diff --git a/theories/Make.streams b/theories/Make.streams
deleted file mode 100644
index ccfab5acfa..0000000000
--- a/theories/Make.streams
+++ /dev/null
@@ -1,4 +0,0 @@
-Streams/Streams.v
-Streams/StreamMemo.v
-
--Q Streams Stdlib.Streams
diff --git a/theories/Make.strings b/theories/Make.strings
deleted file mode 100644
index e7ceaf1353..0000000000
--- a/theories/Make.strings
+++ /dev/null
@@ -1,11 +0,0 @@
-Strings/HexString.v
-Strings/Ascii.v
-Strings/String.v
-Strings/OctalString.v
-Strings/Byte.v
-Strings/BinaryString.v
-Numbers/_Strings/DecimalString.v
-Numbers/_Strings/HexadecimalString.v
-
--Q Strings Stdlib.Strings
--Q Numbers/_Strings Stdlib.Numbers
diff --git a/theories/Make.structures b/theories/Make.structures
deleted file mode 100644
index e0fadee20f..0000000000
--- a/theories/Make.structures
+++ /dev/null
@@ -1,7 +0,0 @@
-Structures/_Def/GenericMinMax.v
-Structures/_Def/Equalities.v
-Structures/_Def/Orders.v
-Structures/_Def/OrdersFacts.v
-Structures/_Def/OrdersTac.v
-
--Q Structures/_Def Stdlib.Structures
diff --git a/theories/Make.unicode b/theories/Make.unicode
deleted file mode 100644
index 41186df3b8..0000000000
--- a/theories/Make.unicode
+++ /dev/null
@@ -1,4 +0,0 @@
-Unicode/Utf8_core.v
-Unicode/Utf8.v
-
--Q Unicode Stdlib.Unicode
diff --git a/theories/Make.vectors b/theories/Make.vectors
deleted file mode 100644
index 78ceb2a199..0000000000
--- a/theories/Make.vectors
+++ /dev/null
@@ -1,9 +0,0 @@
-Vectors/VectorEq.v
-Vectors/VectorDef.v
-Vectors/Vector.v
-Vectors/Fin.v
-Vectors/VectorSpec.v
-Vectors/Bvector.v
-Vectors/FinFun.v
-
--Q Vectors Stdlib.Vectors
diff --git a/theories/Make.wellfounded b/theories/Make.wellfounded
deleted file mode 100644
index f34da0469d..0000000000
--- a/theories/Make.wellfounded
+++ /dev/null
@@ -1,12 +0,0 @@
-Wellfounded/Inclusion.v
-Wellfounded/Wellfounded.v
-Wellfounded/Union.v
-Wellfounded/Transitive_Closure.v
-Wellfounded/Well_Ordering.v
-Wellfounded/Inverse_Image.v
-Wellfounded/Disjoint_Union.v
-Wellfounded/Lexicographic_Product.v
-Wellfounded/Lexicographic_Exponentiation.v
-Wellfounded/List_Extension.v
-
--Q Wellfounded Stdlib.Wellfounded
diff --git a/theories/Make.zarith b/theories/Make.zarith
deleted file mode 100644
index 97f9ee8bd6..0000000000
--- a/theories/Make.zarith
+++ /dev/null
@@ -1,36 +0,0 @@
-Numbers/Natural/Binary/NBinary.v
-ZArith/_All/Zpower.v
-ZArith/_All/Zquot.v
-ZArith/_All/Zpow_facts.v
-ZArith/_All/Zdiv_facts.v
-ZArith/_All/Zgcd_alt.v
-ZArith/_All/Zwf.v
-ZArith/_All/ZArith.v
-ZArith/_All/Zbitwise.v
-ZArith/_All/ZModOffset.v
-ZArith/_All/Zdivisibility.v
-ZArith/_All/Zcong.v
-ZArith/_All/Znumtheory.v
-ZArith/_All/ZNsatz.v
-Numbers/Integer/Binary/ZBinary.v
-Numbers/Integer/NatPairs/ZNatPairs.v
-Numbers/_ZArith/DecimalN.v
-Numbers/_ZArith/DecimalNat.v
-Numbers/_ZArith/DecimalZ.v
-Numbers/_ZArith/DecimalFacts.v
-Numbers/_ZArith/DecimalPos.v
-Numbers/_ZArith/HexadecimalN.v
-Numbers/_ZArith/HexadecimalNat.v
-Numbers/_ZArith/HexadecimalZ.v
-Numbers/_ZArith/HexadecimalFacts.v
-Numbers/_ZArith/HexadecimalPos.v
-btauto/Algebra.v
-btauto/Reflect.v
-btauto/Btauto.v
-
--Q ZArith/_All Stdlib.ZArith
--Q Numbers/Natural/Binary Stdlib.Numbers.Natural.Binary
--Q Numbers/Integer/Binary Stdlib.Numbers.Integer.Binary
--Q Numbers/Integer/NatPairs Stdlib.Numbers.Integer.NatPairs
--Q Numbers/_ZArith Stdlib.Numbers
--Q btauto Stdlib.btauto
diff --git a/theories/Make.zarith-base b/theories/Make.zarith-base
deleted file mode 100644
index 78fd933bce..0000000000
--- a/theories/Make.zarith-base
+++ /dev/null
@@ -1,41 +0,0 @@
-Numbers/Integer/Abstract/ZSgnAbs.v
-Numbers/Integer/Abstract/ZAxioms.v
-Numbers/Integer/Abstract/ZAddOrder.v
-Numbers/Integer/Abstract/ZProperties.v
-Numbers/Integer/Abstract/ZDivTrunc.v
-Numbers/Integer/Abstract/ZParity.v
-Numbers/Integer/Abstract/ZMul.v
-Numbers/Integer/Abstract/ZPow.v
-Numbers/Integer/Abstract/ZAdd.v
-Numbers/Integer/Abstract/ZDivFloor.v
-Numbers/Integer/Abstract/ZMulOrder.v
-Numbers/Integer/Abstract/ZDivEucl.v
-Numbers/Integer/Abstract/ZMaxMin.v
-Numbers/Integer/Abstract/ZGcd.v
-Numbers/Integer/Abstract/ZLt.v
-Numbers/Integer/Abstract/ZLcm.v
-Numbers/Integer/Abstract/ZBase.v
-Numbers/Integer/Abstract/ZBits.v
-ZArith/_Base/BinIntDef.v
-ZArith/_Base/BinInt.v
-ZArith/_Base/Zcompare.v
-ZArith/_Base/Zorder.v
-ZArith/_Base/Zminmax.v
-ZArith/_Base/Zmin.v
-ZArith/_Base/Zmax.v
-ZArith/_Base/Znat.v
-ZArith/_Base/ZArith_dec.v
-ZArith/_Base/Zabs.v
-ZArith/_Base/auxiliary.v
-ZArith/_Base/Zbool.v
-ZArith/_Base/Zmisc.v
-ZArith/_Base/Wf_Z.v
-ZArith/_Base/Zhints.v
-ZArith/_Base/ZArith_base.v
-ZArith/_Base/Zeven.v
-ZArith/_Base/Zpow_alt.v
-ZArith/_Base/Zeuclid.v
-ZArith/_Base/Int.v
-
--Q Numbers/Integer/Abstract Stdlib.Numbers.Integer.Abstract
--Q ZArith/_Base Stdlib.ZArith
diff --git a/theories/Make.zmod b/theories/Make.zmod
deleted file mode 100644
index 134948b1f2..0000000000
--- a/theories/Make.zmod
+++ /dev/null
@@ -1,10 +0,0 @@
-Zmod/Bits.v
-Zmod/Zmod.v
-Zmod/ZmodBase.v
-Zmod/ZmodDef.v
-Zmod/ZmodInv.v
-Zmod/Zstar.v
-Zmod/ZstarBase.v
-Zmod/ZstarDef.v
-
--Q Zmod Stdlib.Zmod
diff --git a/theories/Makefile b/theories/Makefile
index 68dd23a06f..43b64b0c99 100644
--- a/theories/Makefile
+++ b/theories/Makefile
@@ -3,32 +3,12 @@ ROCQMAKEFILE?=$(ROCQBIN)rocq makefile
 ROCQMAKEOPTIONS?=
 ROCQMAKEFILEOPTIONS?=
 
-.PHONY: all
-all: Makefile.coq
-	+$(MAKE) -f $< $(ROCQMAKEOPTIONS)
-
-.PHONY: install
-install: Makefile.coq
-	+$(MAKE) -f $< $(ROCQMAKEOPTIONS) install
+.PHONY: all install clean
+all install clean: Makefile.coq
+	+$(MAKE) -f $< $(ROCQMAKEOPTIONS) $@
 
 Makefile.coq: _CoqProject
 	$(ROCQMAKEFILE) $(ROCQMAKEFILEOPTIONS) -f $< $(shell find . -name "*.v") -o $@
 
-build-%: Makefile-%.coq
-	+$(MAKE) -f $< $(ROCQMAKEOPTIONS)
-
-Makefile-%.coq: Make.%
-	for f in $$(cat $< | sed -e 's/#.*//;s/-.*//' | grep -v '^[ \t]*$$') ; do \
-	  d=$$(dirname $${f}) ; \
-	  if [ $${d%/_*} != $${d} ] ; then \
-	    mkdir -p $${d} ; \
-	    ln -sf ../$$(basename $${f}) $${d} ; \
-	  fi ; \
-	done
-	$(ROCQMAKEFILE) $(ROCQMAKEFILEOPTIONS) -f $< -o $@
-
-install-%: Makefile-%.coq
-	+$(MAKE) -f $< $(ROCQMAKEOPTIONS) install
-
 %.vo: Makefile.coq %.v
 	+$(MAKE) -f $< $(ROCQMAKEOPTIONS) $@
diff --git a/theories/Makefile.coq.local b/theories/Makefile.coq.local
new file mode 100644
index 0000000000..c4413d93a3
--- /dev/null
+++ b/theories/Makefile.coq.local
@@ -0,0 +1,9 @@
+./All.v: ./All.sh $(filter-out ./All.v,$(VFILES))
+	$(HIDE)bash ./$< > $@
+
+./All.vo: ./All.v $(patsubst %.v,%.vo,$(filter-out ./All.v,$(VFILES)))
+
+VFILES+=./All.v
+
+clean::
+	$(HIDE)rm -f ./All.v
diff --git a/theories/dune b/theories/dune
index a930fb90e6..9596d091fa 100644
--- a/theories/dune
+++ b/theories/dune
@@ -7,3 +7,8 @@
  (dev
   (coq
    (flags :standard -w +default))))
+
+(rule
+ (targets All.v)
+ (deps All.sh (source_tree .))
+ (action (with-stdout-to %{targets} (run env sh ./All.sh))))