diff --git a/classical/cardinality.v b/classical/cardinality.v
index 14bc8ef957..7fa86eeb80 100644
--- a/classical/cardinality.v
+++ b/classical/cardinality.v
@@ -2,7 +2,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import finset.
-Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import functions.
 
 (******************************************************************************)
 (*                              Cardinality                                   *)
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 33a8ffbedc..f661c379bc 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
 From mathcomp Require Import ssrint interval.
-Require Import mathcomp_extra boolp.
+From mathcomp.classical Require Import mathcomp_extra boolp.
 
 (******************************************************************************)
 (* This file develops a basic theory of sets and types equipped with a        *)
diff --git a/classical/fsbigop.v b/classical/fsbigop.v
index 2eb96a6ce7..231f18d546 100644
--- a/classical/fsbigop.v
+++ b/classical/fsbigop.v
@@ -1,6 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
-Require Import mathcomp_extra boolp classical_sets functions cardinality.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import functions cardinality.
 
 (******************************************************************************)
 (*                     Finitely-supported big operators                       *)
diff --git a/classical/functions.v b/classical/functions.v
index 6787264c49..e68a8cc8bf 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
-Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 Add Search Blacklist "__canonical__".
 Add Search Blacklist "__functions_".
 Add Search Blacklist "_factory_".
diff --git a/classical/set_interval.v b/classical/set_interval.v
index 4bb4bbc1ac..c03a5b01ae 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -1,7 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
-Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 From HB Require Import structures.
+From mathcomp.classical Require Import functions.
 
 (******************************************************************************)
 (* This files contains lemmas about sets and intervals.                       *)
diff --git a/theories/itv.v b/theories/itv.v
index e7a18d98e2..34ba6dc8d5 100644
--- a/theories/itv.v
+++ b/theories/itv.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
-From mathcomp Require Import interval mathcomp_extra.
-From mathcomp.classical Require Import boolp.
+From mathcomp Require Import interval.
+From mathcomp.classical Require Import mathcomp_extra boolp.
 Require Import signed.
 
 (******************************************************************************)
diff --git a/theories/probability.v b/theories/probability.v
index d3af8238fb..ead0ac27e5 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -1,11 +1,11 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
-Require Import mathcomp_extra boolp reals ereal.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 From HB Require Import structures.
-Require Import classical_sets signed functions topology normedtype cardinality.
-Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral.
-Require Import exp.
+From mathcomp.classical Require Import functions cardinality.
+Require Import reals ereal signed topology normedtype sequences exp esum.
+Require Import measure numfun lebesgue_measure lebesgue_integral.
 
 (******************************************************************************)
 (*                       Probability (experimental)                           *)