diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 9837315..139c81a 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -23,7 +23,6 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-8.18'
           - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-dev'
diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml
index 58f966a..c1aa29a 100644
--- a/.github/workflows/nix-action-8.18.yml
+++ b/.github/workflows/nix-action-8.18.yml
@@ -27,11 +27,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -77,11 +77,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -149,11 +149,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -230,11 +230,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -291,11 +291,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -360,11 +360,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -436,11 +436,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -492,11 +492,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -549,11 +549,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -625,11 +625,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -691,11 +691,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml
index 81771a8..4936ef2 100644
--- a/.github/workflows/nix-action-8.19.yml
+++ b/.github/workflows/nix-action-8.19.yml
@@ -27,11 +27,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -77,11 +77,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -149,11 +149,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -230,11 +230,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -291,11 +291,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -360,11 +360,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -436,11 +436,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -492,11 +492,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -549,11 +549,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -625,11 +625,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -691,11 +691,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml
index d1401ae..0bdcb79 100644
--- a/.github/workflows/nix-action-master.yml
+++ b/.github/workflows/nix-action-master.yml
@@ -28,11 +28,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -79,11 +79,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -127,11 +127,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -183,11 +183,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -256,11 +256,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -313,11 +313,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -394,11 +394,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -456,11 +456,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -525,11 +525,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -601,11 +601,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -657,11 +657,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -714,11 +714,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -790,11 +790,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -856,11 +856,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
@@ -928,11 +928,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
-      uses: cachix/install-nix-action@v20
+      uses: cachix/install-nix-action@v27
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup math-comp
-      uses: cachix/cachix-action@v12
+      uses: cachix/cachix-action@v15
       with:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community
diff --git a/.nix/config.nix b/.nix/config.nix
index 203ea1f..08c6e31 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -64,10 +64,13 @@
     coq.override.version = "master";
     bignums.override.version = "master";
     paramcoq.override.version = "master";
-    coq-elpi.override.version = "coq-master";
+    coq-elpi.override.version = "master";
     hierarchy-builder.override.version = "master";
     mathcomp.override.version = "master";
   };
+  "master".ocamlPackages = {
+    elpi.override.version = "1.19.2";
+  };
   };
 
   ## Cachix caches to use in CI
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
index 77c1629..3ac5205 100644
--- a/.nix/coq-nix-toolbox.nix
+++ b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"e9a1613edc5b5c3f7124f5a4a83169870c8f4f95"
+"66abb687550ec2800bc1724036cfb5d9656c901c"
diff --git a/meta.yml b/meta.yml
index be363f4..cd8f27d 100644
--- a/meta.yml
+++ b/meta.yml
@@ -55,8 +55,6 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.17'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.18'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.19'
diff --git a/theories/cauchyreals.v b/theories/cauchyreals.v
index 8be0693..c94caa8 100644
--- a/theories/cauchyreals.v
+++ b/theories/cauchyreals.v
@@ -1,12 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
-From mathcomp
-Require Import bigop order ssralg ssrnum ssrint rat poly polydiv polyorder.
-From mathcomp
-Require Import perm matrix mxpoly polyXY binomial bigenough.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype bigop binomial order perm ssralg poly.
+From mathcomp Require Import polydiv ssrnum ssrint rat matrix mxpoly polyXY.
+From mathcomp Require Import bigenough polyorder.
 
 (***************************************************************************)
 (* This is a standalone construction of Cauchy reals over an arbitrary     *)
@@ -15,7 +12,7 @@ Require Import perm matrix mxpoly polyXY binomial bigenough.
 (*               cannot be equipped with any ssreflect algebraic structure *)
 (***************************************************************************)
 
-Import Order.TTheory GRing.Theory Num.Theory Num.Def BigEnough.
+Import Order.TTheory GRing.Theory Num.Theory BigEnough.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -107,7 +104,7 @@ Lemma poly_bound_ge0 p a r : 0 <= poly_bound p a r.
 Proof. by rewrite ltW // poly_bound_gt0. Qed.
 
 Definition poly_accr_bound (p : {poly F}) (a r : F) : F
-  := (maxr 1 (2%:R * r)) ^+ (size p).-1
+  := (Num.max 1 (2%:R * r)) ^+ (size p).-1
   * (1 + \sum_(i < (size p).-1) poly_bound p^`N(i.+1) a r).
 
 Lemma poly_accr_bound1P p a r x y :
@@ -131,7 +128,7 @@ have := le_trans (ler_norm_sum _ _ _); apply.
 rewrite ler_sum // => i _.
 rewrite exprSr mulrA !normrM mulrC ler_wpM2l ?normr_ge0 //.
 suff /ler_wpM2l /le_trans :
-  `|(y - x) ^+ i| <=  maxr 1 (2%:R * r) ^+ (size p).-1.
+  `|(y - x) ^+ i| <=  Num.max 1 (2%:R * r) ^+ (size p).-1.
   apply; rewrite ?normr_ge0 // mulrC ler_wpM2l ?poly_boundP //.
   by rewrite ?exprn_ge0 // le_max ler01 mulr_ge0 ?ler0n ?ltW.
 case: (leP _ 1)=> hr.
@@ -205,7 +202,7 @@ Variable F : realFieldType.
 Local Open Scope ring_scope.
 
 Definition poly_accr_bound2 (p : {poly F}) (a r : F) : F
-  := (maxr 1 (2%:R * r)) ^+ (size p).-2
+  := (Num.max 1 (2%:R * r)) ^+ (size p).-2
   * (1 + \sum_(i < (size p).-2) poly_bound p^`N(i.+2) a r).
 
 Lemma poly_accr_bound2_gt0 p a r : 0 < poly_accr_bound2 p a r.
@@ -249,7 +246,7 @@ have := le_trans (ler_norm_sum _ _ _); apply.
 rewrite ler_sum // => i _ /=; rewrite /bump /= !add1n.
 rewrite normrM normrX 3!exprSr expr1 !mulrA !ler_wpM2r ?normr_ge0 //.
 suff /ler_wpM2l /le_trans :
-  `|(y - x)| ^+ i <=  maxr 1 (2%:R * r) ^+ (size p^`()).-1.
+  `|(y - x)| ^+ i <= Num.max 1 (2%:R * r) ^+ (size p^`()).-1.
   apply; rewrite ?normr_ge0 // mulrC ler_wpM2l ?poly_boundP //.
   by rewrite ?exprn_ge0 // le_max ler01 mulr_ge0 ?ler0n ?ltW.
 case: (leP _ 1)=> hr.
@@ -341,8 +338,8 @@ by rewrite -normfV -normrM ler_normr lexx ?orbT.
 Qed.
 
 Definition merge_intervals (ar1 ar2 : F * F) :=
-  let l := minr (ar1.1 - ar1.2) (ar2.1 - ar2.2) in
-  let u := maxr (ar1.1 + ar1.2) (ar2.1 + ar2.2) in
+  let l := Num.min (ar1.1 - ar1.2) (ar2.1 - ar2.2) in
+  let u := Num.max (ar1.1 + ar1.2) (ar2.1 + ar2.2) in
     ((l + u) / 2%:R, (u - l) / 2%:R).
 Local Notation center ar1 ar2 := ((merge_intervals ar1 ar2).1).
 Local Notation radius ar1 ar2 := ((merge_intervals ar1 ar2).2).
@@ -354,7 +351,7 @@ Lemma split_interval (a1 a2 r1 r2 x : F) :
 Proof.
 move=> r1_gt0 r2_gt0 le_ar.
 rewrite /merge_intervals /=.
-set l : F := minr _ _; set u : F := maxr _ _.
+set l : F := Num.min _ _; set u : F := Num.max _ _.
 rewrite ler_pdivlMr ?gtr0E // -{2}[2%:R]ger0_norm ?ger0E //.
 rewrite -normrM mulrBl mulfVK ?pnatr_eq0 // ler_distl.
 rewrite opprB addrCA addrK (addrC (l + u)) addrA addrNK.
@@ -406,7 +403,7 @@ move=> [] accr2_p; last first.
   by rewrite mulrC ler_wpM2r // ltW.
 case: accr2_p=> [[k2 k2_gt0 hk2]] h2.
 left; split; last by move=> x; rewrite split_interval // => /orP [/h1|/h2].
-exists (minr k1 k2); first by rewrite lt_min k1_gt0.
+exists (Num.min k1 k2); first by rewrite lt_min k1_gt0.
 move=> x y neq_xy; rewrite !split_interval //.
 wlog lt_xy: x y neq_xy / y < x.
   move=> hwlog; have [] := ltrP y x; first exact: hwlog.
@@ -457,7 +454,6 @@ End monotony.
 
 Section CauchyReals.
 
-Local Open Scope nat_scope.
 Local Open Scope creal_scope.
 Local Open Scope ring_scope.
 
@@ -873,7 +869,7 @@ Notation "x - y" := (x + - y)%CR : creal_scope.
 Lemma ubound_subproof (x : creal) : {b : F | b > 0 & forall i, `|x i| <= b}.
 Proof.
 pose_big_enough i; first set b := 1 + `|x i|.
-  exists (foldl maxr b [seq `|x n| | n <- iota 0 i]) => [|n].
+  exists (foldl Num.max b [seq `|x n| | n <- iota 0 i]) => [|n].
     have : 0 < b by rewrite ltr_pwDl.
     by elim: iota b => //= a l IHl b b_gt0; rewrite IHl ?lt_max ?b_gt0.
   have [|le_in] := (ltnP n i).
@@ -1360,7 +1356,7 @@ wlog : p px_neq0 / (0 < p^`().[x])%CR.
 move=> px_gt0.
 pose b1 := poly_accr_bound p^`() 0 (1 + ubound x).
 pose b2 := poly_accr_bound2 p 0 (1 + ubound x).
-pose r : F := minr 1 (minr
+pose r : F := Num.min 1 (Num.min
   (diff px_gt0 / 4%:R / b1)
   (diff px_gt0 / 4%:R / b2 / 2%:R)).
 exists r.
@@ -1504,7 +1500,7 @@ by rewrite (le_trans _ (bound_poly_boundP _ 0%N _ _ _ _)) ?poly_bound_ge0.
 Qed.
 
 Definition bound_poly_accr_bound (z : creal) (q : {poly {poly F}}) (a r : F) :=
-   maxr 1 (2%:R * r) ^+ (sizeY q).-1 *
+   Num.max 1 (2%:R * r) ^+ (sizeY q).-1 *
    (1 + \sum_(i < (sizeY q).-1) bound_poly_bound z q a r i).
 
 Lemma bound_poly_accr_boundP (z : creal) i (q : {poly {poly F}}) (a r : F) :
diff --git a/theories/complex.v b/theories/complex.v
index 7823df5..4728d02 100644
--- a/theories/complex.v
+++ b/theories/complex.v
@@ -1,14 +1,10 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From HB Require Import structures.
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
-From mathcomp
-Require Import bigop order ssralg ssrint div ssrnum rat poly closed_field.
-From mathcomp
-Require Import polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg.
-From mathcomp Require Import mxpoly.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype tuple bigop binomial order ssralg.
+From mathcomp Require Import zmodp poly ssrnum ssrint archimedean rat matrix.
+From mathcomp Require Import mxalgebra mxpoly closed_field polyrcf realalg.
 
 (**********************************************************************)
 (*   This files defines the extension R[i] of a real field R,         *)
diff --git a/theories/mxtens.v b/theories/mxtens.v
index c37ae59..1b3054e 100644
--- a/theories/mxtens.v
+++ b/theories/mxtens.v
@@ -1,17 +1,13 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
-From mathcomp
-Require Import bigop ssralg matrix zmodp div.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype bigop ssralg zmodp matrix.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import GRing.Theory.
-Local Open Scope nat_scope.
 Local Open Scope ring_scope.
 
 Section ExtraBigOp.
diff --git a/theories/ordered_qelim.v b/theories/ordered_qelim.v
index a2c776f..aa494aa 100644
--- a/theories/ordered_qelim.v
+++ b/theories/ordered_qelim.v
@@ -1,14 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From HB Require Import structures.
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype.
-From mathcomp
-Require Import bigop order ssralg finset fingroup zmodp.
-From mathcomp
-Require Import poly ssrnum.
-
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
+From mathcomp Require Import choice fintype bigop finset order fingroup.
+From mathcomp Require Import ssralg zmodp poly ssrnum.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/polyorder.v b/theories/polyorder.v
index 5e425ec..ccb297e 100644
--- a/theories/polyorder.v
+++ b/theories/polyorder.v
@@ -1,15 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
-From mathcomp
-Require Import ssralg poly ssrnum zmodp polydiv interval.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype ssralg zmodp poly polydiv ssrnum interval.
 
-Import GRing.Theory.
-Import Num.Theory.
-
-Import Pdiv.Idomain.
+Import GRing.Theory Num.Theory Pdiv.Idomain.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/polyrcf.v b/theories/polyrcf.v
index be486e6..b6f5886 100644
--- a/theories/polyrcf.v
+++ b/theories/polyrcf.v
@@ -1,7 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-From mathcomp Require Import all_ssreflect all_algebra.
-Require Import polyorder.
+From mathcomp Require Import all_ssreflect all_algebra polyorder.
 
 (****************************************************************************)
 (* This files contains basic (and unformatted) theory for polynomials       *)
@@ -36,7 +35,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Local Open Scope nat_scope.
 Local Open Scope ring_scope.
 
 Local Notation noroot p := (forall x, ~~ root p x).
diff --git a/theories/qe_rcf.v b/theories/qe_rcf.v
index 4d9201f..b61334d 100644
--- a/theories/qe_rcf.v
+++ b/theories/qe_rcf.v
@@ -1,16 +1,9 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
-From mathcomp
-Require Import finfun path matrix.
-From mathcomp
-Require Import bigop order ssralg poly polydiv ssrnum zmodp div ssrint.
-From mathcomp
-Require Import polyorder polyrcf interval polyXY.
-From mathcomp
-Require Import qe_rcf_th ordered_qelim mxtens.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype finfun bigop order ssralg zmodp.
+From mathcomp Require Import poly polydiv ssrnum ssrint interval matrix polyXY.
+From mathcomp Require Import polyorder polyrcf mxtens qe_rcf_th ordered_qelim.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -18,7 +11,6 @@ Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Theory.
 
-Local Open Scope nat_scope.
 Local Open Scope ring_scope.
 
 Definition grab (X Y : Type) (pattern : Y -> Prop) (P : Prop -> Prop) 
diff --git a/theories/qe_rcf_th.v b/theories/qe_rcf_th.v
index 760ea34..7d7cd0e 100644
--- a/theories/qe_rcf_th.v
+++ b/theories/qe_rcf_th.v
@@ -1,15 +1,14 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import all_ssreflect all_algebra.
-Require Import polyorder polyrcf mxtens.
+From mathcomp Require Import polyorder polyrcf mxtens.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import Order.TTheory GRing.Theory Num.Theory Num.Def Pdiv.Ring Pdiv.ComRing.
+Import Order.TTheory GRing.Theory Num.Theory Pdiv.Ring Pdiv.ComRing.
 
-Local Open Scope nat_scope.
 Local Open Scope ring_scope.
 
 Section extra.
@@ -211,7 +210,7 @@ Notation midf a b := ((a + b) / 2%:~R).
 
 (* Constraints and Tarski queries *)
 
-Local Notation sgp_is q s := (fun x => (sgr q.[x] == s)).
+Local Notation sgp_is q s := (fun x => (Num.sg q.[x] == s)).
 
 Definition constraints (z : seq R) (sq : seq {poly R}) (sigma : seq int) :=
   (\sum_(x <- z) \prod_(i < size sq) (sgz (sq`_i).[x] == (sigma`_i)%R))%N.
diff --git a/theories/realalg.v b/theories/realalg.v
index 31bd220..7b930de 100644
--- a/theories/realalg.v
+++ b/theories/realalg.v
@@ -1,9 +1,8 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra all_field.
-From mathcomp Require Import archimedean bigenough.
-Require Import polyorder cauchyreals.
+From mathcomp Require Import all_ssreflect all_algebra all_field bigenough.
+From mathcomp Require Import polyorder cauchyreals.
 
 (*************************************************************************)
 (* This files constructs the real closure of an archimedian field in the *)