diff --git a/proofs/arch/arch_decl.v b/proofs/arch/arch_decl.v
index f607225ec..81f8b4300 100644
--- a/proofs/arch/arch_decl.v
+++ b/proofs/arch/arch_decl.v
@@ -1,6 +1,6 @@
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import
   Relation_Operators
diff --git a/proofs/arch/arch_extra.v b/proofs/arch/arch_extra.v
index 1f399af8f..89ba47510 100644
--- a/proofs/arch/arch_extra.v
+++ b/proofs/arch/arch_extra.v
@@ -1,6 +1,6 @@
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import xseq strings utils var type values sopn expr fexpr arch_decl.
 Require Import compiler_util.
 
diff --git a/proofs/arch/arch_sem.v b/proofs/arch/arch_sem.v
index 981a0955c..518894bcf 100644
--- a/proofs/arch/arch_sem.v
+++ b/proofs/arch/arch_sem.v
@@ -1,5 +1,5 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import word_ssrZ.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype finfun.
+From mathcomp Require Import ssralg word_ssrZ.
 Require oseq.
 Require Import ZArith
 utils
diff --git a/proofs/arch/arch_utils.v b/proofs/arch/arch_utils.v
index de902bf14..42042b654 100644
--- a/proofs/arch/arch_utils.v
+++ b/proofs/arch/arch_utils.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
 
 Require Import
   type
diff --git a/proofs/arch/asm_gen.v b/proofs/arch/asm_gen.v
index b1de0ab4b..db77e4d08 100644
--- a/proofs/arch/asm_gen.v
+++ b/proofs/arch/asm_gen.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 Require Import
   oseq
   compiler_util
@@ -11,7 +11,6 @@ Require Import
   arch_decl
   arch_extra.
 Import Utf8 String.
-Import all_ssreflect.
 Import compiler_util.
 
 Set Implicit Arguments.
diff --git a/proofs/arch/asm_gen_proof.v b/proofs/arch/asm_gen_proof.v
index 833498276..f06bc10b6 100644
--- a/proofs/arch/asm_gen_proof.v
+++ b/proofs/arch/asm_gen_proof.v
@@ -1,4 +1,5 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
+From mathcomp Require Import fintype finfun ssralg.
 From Coq Require Import Relation_Operators.
 Require Import
   oseq
diff --git a/proofs/arch/label.v b/proofs/arch/label.v
index 65d0edee7..f09fa3408 100644
--- a/proofs/arch/label.v
+++ b/proofs/arch/label.v
@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 Require Import global Utf8.
 
 Set   Implicit Arguments.
diff --git a/proofs/arch/sem_params_of_arch_extra.v b/proofs/arch/sem_params_of_arch_extra.v
index 4f0a8d011..85d110e6a 100644
--- a/proofs/arch/sem_params_of_arch_extra.v
+++ b/proofs/arch/sem_params_of_arch_extra.v
@@ -1,7 +1,3 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
-
 Require Import
   sem_params
   syscall.
diff --git a/proofs/compiler/allocation.v b/proofs/compiler/allocation.v
index 18ec44d27..95d757b94 100644
--- a/proofs/compiler/allocation.v
+++ b/proofs/compiler/allocation.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From mathcomp Require Import word_ssrZ.
 Require Import expr compiler_util ZArith.
 Import Utf8.
diff --git a/proofs/compiler/allocation_proof.v b/proofs/compiler/allocation_proof.v
index 9ef00cbfe..9c21e529a 100644
--- a/proofs/compiler/allocation_proof.v
+++ b/proofs/compiler/allocation_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 Require Import psem compiler_util.
 Require Export allocation.
 
diff --git a/proofs/compiler/arch_params.v b/proofs/compiler/arch_params.v
index d38cf6cc3..a8916d871 100644
--- a/proofs/compiler/arch_params.v
+++ b/proofs/compiler/arch_params.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
 Require Import
   compiler_util
   expr.
diff --git a/proofs/compiler/arch_params_proof.v b/proofs/compiler/arch_params_proof.v
index 88437190a..95b113452 100644
--- a/proofs/compiler/arch_params_proof.v
+++ b/proofs/compiler/arch_params_proof.v
@@ -1,5 +1,4 @@
-
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 Require Import
   compiler_util
   expr
diff --git a/proofs/compiler/arm.v b/proofs/compiler/arm.v
index 9f66d5730..7e5f7d357 100644
--- a/proofs/compiler/arm.v
+++ b/proofs/compiler/arm.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 
 Require Import utils.
 Require Import arch_decl.
diff --git a/proofs/compiler/arm_decl.v b/proofs/compiler/arm_decl.v
index fb045f3e9..788b08853 100644
--- a/proofs/compiler/arm_decl.v
+++ b/proofs/compiler/arm_decl.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype fintype ssralg.
 From mathcomp Require Import word_ssrZ.
 
 Require Import
diff --git a/proofs/compiler/arm_extra.v b/proofs/compiler/arm_extra.v
index 6f5db9881..6127c199a 100644
--- a/proofs/compiler/arm_extra.v
+++ b/proofs/compiler/arm_extra.v
@@ -1,7 +1,5 @@
 From HB Require Import structures.
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 
 Require Import
   compiler_util
diff --git a/proofs/compiler/arm_facts.v b/proofs/compiler/arm_facts.v
index 499fc7ed3..4d97eea4d 100644
--- a/proofs/compiler/arm_facts.v
+++ b/proofs/compiler/arm_facts.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From Coq Require Import ZArith.
 
 Require Import
diff --git a/proofs/compiler/arm_instr_decl.v b/proofs/compiler/arm_instr_decl.v
index 819f6eb73..dc285931d 100644
--- a/proofs/compiler/arm_instr_decl.v
+++ b/proofs/compiler/arm_instr_decl.v
@@ -3,10 +3,8 @@
    These are the THUMB instructions of ARMv7-M, the instruction set of the M4
    processor. *)
 
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
-From mathcomp Require Import word_ssrZ.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype fintype.
+From mathcomp Require Import ssralg word_ssrZ.
 
 Require Import
   sem_type
diff --git a/proofs/compiler/arm_instr_decl_lemmas.v b/proofs/compiler/arm_instr_decl_lemmas.v
index dcdca2505..a15601f76 100644
--- a/proofs/compiler/arm_instr_decl_lemmas.v
+++ b/proofs/compiler/arm_instr_decl_lemmas.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import word_ssrZ.
 
 Require Import
diff --git a/proofs/compiler/arm_lowering.v b/proofs/compiler/arm_lowering.v
index 6aad46dc7..230d69060 100644
--- a/proofs/compiler/arm_lowering.v
+++ b/proofs/compiler/arm_lowering.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
 Require Import
diff --git a/proofs/compiler/arm_lowering_proof.v b/proofs/compiler/arm_lowering_proof.v
index 3d2c0e00f..d93d55cd2 100644
--- a/proofs/compiler/arm_lowering_proof.v
+++ b/proofs/compiler/arm_lowering_proof.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssralg.
 Import
   Order.POrderTheory
   Order.TotalTheory.
diff --git a/proofs/compiler/arm_params.v b/proofs/compiler/arm_params.v
index 99e5c4ed0..697cecf38 100644
--- a/proofs/compiler/arm_params.v
+++ b/proofs/compiler/arm_params.v
@@ -1,7 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
-
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 
 Require Import
diff --git a/proofs/compiler/arm_params_common.v b/proofs/compiler/arm_params_common.v
index 85d6ae951..49024066d 100644
--- a/proofs/compiler/arm_params_common.v
+++ b/proofs/compiler/arm_params_common.v
@@ -1,7 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
-
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import word_ssrZ.
 
 Require Import
diff --git a/proofs/compiler/arm_params_common_proof.v b/proofs/compiler/arm_params_common_proof.v
index 6b87351e3..a13f1d340 100644
--- a/proofs/compiler/arm_params_common_proof.v
+++ b/proofs/compiler/arm_params_common_proof.v
@@ -1,8 +1,5 @@
 From Coq Require Import Lia.
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
-
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
 Require Import
diff --git a/proofs/compiler/arm_params_core.v b/proofs/compiler/arm_params_core.v
index 0f767bb5a..c7df32322 100644
--- a/proofs/compiler/arm_params_core.v
+++ b/proofs/compiler/arm_params_core.v
@@ -1,7 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
-
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype.
 From mathcomp Require Import word_ssrZ.
 
 Require Import
diff --git a/proofs/compiler/arm_params_core_proof.v b/proofs/compiler/arm_params_core_proof.v
index 50ff63ab7..4e707f6e6 100644
--- a/proofs/compiler/arm_params_core_proof.v
+++ b/proofs/compiler/arm_params_core_proof.v
@@ -1,8 +1,5 @@
 From Coq Require Import Lia.
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
-
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
 Require Import
diff --git a/proofs/compiler/arm_params_proof.v b/proofs/compiler/arm_params_proof.v
index d97859133..7eecdbae0 100644
--- a/proofs/compiler/arm_params_proof.v
+++ b/proofs/compiler/arm_params_proof.v
@@ -1,5 +1,6 @@
 From Coq Require Import Relations.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat finfun.
+From mathcomp Require Import ssralg.
 From mathcomp Require Import word_ssrZ.
 
 Require Import oseq.
diff --git a/proofs/compiler/arm_stack_zeroization.v b/proofs/compiler/arm_stack_zeroization.v
index b8f3a83a1..fb4d05f53 100644
--- a/proofs/compiler/arm_stack_zeroization.v
+++ b/proofs/compiler/arm_stack_zeroization.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 
 Require Import
   expr
diff --git a/proofs/compiler/arm_stack_zeroization_proof.v b/proofs/compiler/arm_stack_zeroization_proof.v
index 85e5bdb49..e1f6d892c 100644
--- a/proofs/compiler/arm_stack_zeroization_proof.v
+++ b/proofs/compiler/arm_stack_zeroization_proof.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import Lia.
 
diff --git a/proofs/compiler/array_copy.v b/proofs/compiler/array_copy.v
index e16885b02..9b1b97f93 100644
--- a/proofs/compiler/array_copy.v
+++ b/proofs/compiler/array_copy.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 Require Import
   compiler_util
   expr
diff --git a/proofs/compiler/array_copy_proof.v b/proofs/compiler/array_copy_proof.v
index ae1972713..2396a4e96 100644
--- a/proofs/compiler/array_copy_proof.v
+++ b/proofs/compiler/array_copy_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith Lia.
 Require Import array_copy psem.
diff --git a/proofs/compiler/array_expansion.v b/proofs/compiler/array_expansion.v
index 8aa704120..b16a991f4 100644
--- a/proofs/compiler/array_expansion.v
+++ b/proofs/compiler/array_expansion.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From mathcomp Require Import word_ssrZ.
 Require Import expr.
 Require Import compiler_util ZArith.
diff --git a/proofs/compiler/array_expansion_proof.v b/proofs/compiler/array_expansion_proof.v
index 29ea2617c..e8bc37fd9 100644
--- a/proofs/compiler/array_expansion_proof.v
+++ b/proofs/compiler/array_expansion_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From mathcomp Require Import word_ssrZ.
 Require Import psem array_expansion compiler_util ZArith.
 Import Utf8 Lia.
diff --git a/proofs/compiler/array_init.v b/proofs/compiler/array_init.v
index d29eff5c2..1519ff26d 100644
--- a/proofs/compiler/array_init.v
+++ b/proofs/compiler/array_init.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 Require Import ZArith.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 Require Import expr compiler_util.
 
 Set Implicit Arguments.
diff --git a/proofs/compiler/array_init_proof.v b/proofs/compiler/array_init_proof.v
index 06bf695b1..1018d5236 100644
--- a/proofs/compiler/array_init_proof.v
+++ b/proofs/compiler/array_init_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import psem compiler_util.
 Require Export array_init.
 Import Utf8.
diff --git a/proofs/compiler/byteset.v b/proofs/compiler/byteset.v
index 2cb5fda54..7de764a11 100644
--- a/proofs/compiler/byteset.v
+++ b/proofs/compiler/byteset.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
 Require Import utils Wellfounded.
 Import Lexicographic_Product Relation_Operators.
 
diff --git a/proofs/compiler/compiler.v b/proofs/compiler/compiler.v
index 31f51a0a4..677b0f369 100644
--- a/proofs/compiler/compiler.v
+++ b/proofs/compiler/compiler.v
@@ -1,5 +1,6 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype fintype.
+From mathcomp Require Import ssralg.
 Require Import ZArith.
 Require Import Utf8.
 
diff --git a/proofs/compiler/compiler_proof.v b/proofs/compiler/compiler_proof.v
index 61295a875..5d92c144a 100644
--- a/proofs/compiler/compiler_proof.v
+++ b/proofs/compiler/compiler_proof.v
@@ -1,4 +1,5 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
+From mathcomp Require Import fintype finfun ssralg.
 
 Require Import
   arch_params_proof
diff --git a/proofs/compiler/compiler_util.v b/proofs/compiler/compiler_util.v
index 7b81d30bf..da6e15c95 100644
--- a/proofs/compiler/compiler_util.v
+++ b/proofs/compiler/compiler_util.v
@@ -1,5 +1,5 @@
 Require Import ZArith Setoid Morphisms.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 Require Import expr fexpr.
 
 Set Implicit Arguments.
diff --git a/proofs/compiler/constant_prop.v b/proofs/compiler/constant_prop.v
index cce4df467..d213117dc 100644
--- a/proofs/compiler/constant_prop.v
+++ b/proofs/compiler/constant_prop.v
@@ -1,8 +1,8 @@
 (* ** Imports and settings *)
 From HB Require Import structures.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import expr ZArith sem_op_typed compiler_util.
-Import all_ssreflect ssralg ssrnum.
 Import Utf8.
 Import oseq.
 Require Import flag_combination.
diff --git a/proofs/compiler/constant_prop_proof.v b/proofs/compiler/constant_prop_proof.v
index a8c7c9702..3d91f3b80 100644
--- a/proofs/compiler/constant_prop_proof.v
+++ b/proofs/compiler/constant_prop_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 Require Import psem compiler_util.
 Require Export constant_prop.
 
diff --git a/proofs/compiler/dead_calls.v b/proofs/compiler/dead_calls.v
index bf918c127..8fc54af2a 100644
--- a/proofs/compiler/dead_calls.v
+++ b/proofs/compiler/dead_calls.v
@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 (* ------- *) Require Import expr compiler_util gen_map.
 (* ------- *) (* - *) Import PosSet.
 Import  Utf8.
diff --git a/proofs/compiler/dead_calls_proof.v b/proofs/compiler/dead_calls_proof.v
index 25817d634..e2f058f05 100644
--- a/proofs/compiler/dead_calls_proof.v
+++ b/proofs/compiler/dead_calls_proof.v
@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 (* ------- *) Require Import expr compiler_util psem gen_map dead_calls.
 (* ------- *) (* - *) Import PosSet.
 Import Utf8 xseq.
diff --git a/proofs/compiler/dead_code.v b/proofs/compiler/dead_code.v
index afc65e096..960c8eed0 100644
--- a/proofs/compiler/dead_code.v
+++ b/proofs/compiler/dead_code.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import expr compiler_util ZArith.
 
 Set Implicit Arguments.
diff --git a/proofs/compiler/dead_code_proof.v b/proofs/compiler/dead_code_proof.v
index c143b5f02..58b5ccbb1 100644
--- a/proofs/compiler/dead_code_proof.v
+++ b/proofs/compiler/dead_code_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import psem compiler_util.
 Require Export dead_code.
 Import Utf8.
diff --git a/proofs/compiler/direct_call_proof.v b/proofs/compiler/direct_call_proof.v
index 3a1969c79..9f4bea0a0 100644
--- a/proofs/compiler/direct_call_proof.v
+++ b/proofs/compiler/direct_call_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 Require Import varmap psem.
 
 Import Utf8.
diff --git a/proofs/compiler/inline.v b/proofs/compiler/inline.v
index 717357c52..2968588eb 100644
--- a/proofs/compiler/inline.v
+++ b/proofs/compiler/inline.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 Require Import ZArith.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 Require Import expr compiler_util allocation.
 
 Set Implicit Arguments.
diff --git a/proofs/compiler/inline_proof.v b/proofs/compiler/inline_proof.v
index 3c993650d..671153204 100644
--- a/proofs/compiler/inline_proof.v
+++ b/proofs/compiler/inline_proof.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 Require Import ZArith.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import psem allocation_proof compiler_util.
 Require Export inline.
 
diff --git a/proofs/compiler/lea.v b/proofs/compiler/lea.v
index e6ea8a2d8..de95bf905 100644
--- a/proofs/compiler/lea.v
+++ b/proofs/compiler/lea.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 Require Import Utf8.
 Require Import expr.
diff --git a/proofs/compiler/lea_proof.v b/proofs/compiler/lea_proof.v
index 825ea7e23..7f3dc70aa 100644
--- a/proofs/compiler/lea_proof.v
+++ b/proofs/compiler/lea_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 Require Import oseq.
 Require Import psem compiler_util.
 Require Import fexpr fexpr_sem fexpr_facts.
diff --git a/proofs/compiler/linear_util.v b/proofs/compiler/linear_util.v
index ba8b8f0e7..d649a5cf6 100644
--- a/proofs/compiler/linear_util.v
+++ b/proofs/compiler/linear_util.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import expr label linear.
 Require Import seq_extra compiler_util.
 
diff --git a/proofs/compiler/linearization.v b/proofs/compiler/linearization.v
index 1917623d2..4e17e601a 100644
--- a/proofs/compiler/linearization.v
+++ b/proofs/compiler/linearization.v
@@ -2,7 +2,7 @@
 
 (* ** Imports and settings *)
 
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
 Require Import ZArith.
 Require Import Utf8.
 Import Relations.
diff --git a/proofs/compiler/linearization_proof.v b/proofs/compiler/linearization_proof.v
index 1c404b8e0..a8b5e2fac 100644
--- a/proofs/compiler/linearization_proof.v
+++ b/proofs/compiler/linearization_proof.v
@@ -2,7 +2,7 @@
 From Coq
 Require Import Setoid Morphisms Lia.
 
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype ssralg.
 Require Import ZArith Utf8.
         Import Relations.
 
diff --git a/proofs/compiler/lower_spill.v b/proofs/compiler/lower_spill.v
index 26a678121..af082835d 100644
--- a/proofs/compiler/lower_spill.v
+++ b/proofs/compiler/lower_spill.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import pseudo_operator expr compiler_util ZArith.
 
 Set Implicit Arguments.
diff --git a/proofs/compiler/lower_spill_proof.v b/proofs/compiler/lower_spill_proof.v
index 3b9ff8060..65f47bd42 100644
--- a/proofs/compiler/lower_spill_proof.v
+++ b/proofs/compiler/lower_spill_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import psem compiler_util.
 Require Export pseudo_operator lower_spill.
 Import Utf8.
diff --git a/proofs/compiler/lowering.v b/proofs/compiler/lowering.v
index 8c15dc0e1..dc6e95902 100644
--- a/proofs/compiler/lowering.v
+++ b/proofs/compiler/lowering.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import word_ssrZ.
 Require Import compiler_util expr.
 
 Section LOWERING.
diff --git a/proofs/compiler/makeReferenceArguments.v b/proofs/compiler/makeReferenceArguments.v
index d1e6a892a..b7bc5e2f4 100644
--- a/proofs/compiler/makeReferenceArguments.v
+++ b/proofs/compiler/makeReferenceArguments.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 From Coq Require Import HexadecimalString ZArith.
 Require Import gen_map expr compiler_util.
 
diff --git a/proofs/compiler/makeReferenceArguments_proof.v b/proofs/compiler/makeReferenceArguments_proof.v
index 41c5c57b5..4cf5282ec 100644
--- a/proofs/compiler/makeReferenceArguments_proof.v
+++ b/proofs/compiler/makeReferenceArguments_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 Require Import psem compiler_util.
 Require Export makeReferenceArguments.
 Import Utf8.
diff --git a/proofs/compiler/merge_varmaps.v b/proofs/compiler/merge_varmaps.v
index b449c0a9f..a5dc81840 100644
--- a/proofs/compiler/merge_varmaps.v
+++ b/proofs/compiler/merge_varmaps.v
@@ -1,8 +1,8 @@
 (*
 *)
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import one_varmap.
 Import Utf8.
-Import all_ssreflect.
 Import expr compiler_util.
 
 Set Implicit Arguments.
diff --git a/proofs/compiler/merge_varmaps_proof.v b/proofs/compiler/merge_varmaps_proof.v
index 500f35896..a58a2838e 100644
--- a/proofs/compiler/merge_varmaps_proof.v
+++ b/proofs/compiler/merge_varmaps_proof.v
@@ -1,9 +1,9 @@
 (*
 *)
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 Require Import sem_one_varmap sem_one_varmap_facts merge_varmaps psem_facts.
 Require Import seq_extra.
 Import Utf8.
-Import all_ssreflect ssralg ssrnum.
 Import word_ssrZ.
 Import psem.
 Import merge_varmaps.
diff --git a/proofs/compiler/propagate_inline.v b/proofs/compiler/propagate_inline.v
index 2e59d7602..23eeca010 100644
--- a/proofs/compiler/propagate_inline.v
+++ b/proofs/compiler/propagate_inline.v
@@ -1,9 +1,9 @@
 (* ** Imports and settings *)
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 Require Import compiler_util expr ZArith constant_prop.
 Require Import
   flag_combination.
-Import all_ssreflect.
 Import Utf8.
 
 Set Implicit Arguments.
diff --git a/proofs/compiler/propagate_inline_proof.v b/proofs/compiler/propagate_inline_proof.v
index 4e5ea8a9d..cd79de5df 100644
--- a/proofs/compiler/propagate_inline_proof.v
+++ b/proofs/compiler/propagate_inline_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import psem psem_facts constant_prop constant_prop_proof.
 Require Export propagate_inline.
 
diff --git a/proofs/compiler/remove_globals.v b/proofs/compiler/remove_globals.v
index f691b843d..6311f1e65 100644
--- a/proofs/compiler/remove_globals.v
+++ b/proofs/compiler/remove_globals.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import xseq.
 Require Import expr compiler_util ZArith.
diff --git a/proofs/compiler/remove_globals_proof.v b/proofs/compiler/remove_globals_proof.v
index feed777e9..4ae2a89df 100644
--- a/proofs/compiler/remove_globals_proof.v
+++ b/proofs/compiler/remove_globals_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import xseq.
 Require Import compiler_util ZArith expr psem remove_globals low_memory.
diff --git a/proofs/compiler/slh_lowering.v b/proofs/compiler/slh_lowering.v
index 8add4d98b..d9577e7ba 100644
--- a/proofs/compiler/slh_lowering.v
+++ b/proofs/compiler/slh_lowering.v
@@ -16,9 +16,7 @@
    will replace it with [shp_lower ... SLHprotect_ptr ...] when the pointer
    becomes a register. *)
 
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 
 Require Import expr.
 Require constant_prop flag_combination.
diff --git a/proofs/compiler/slh_lowering_proof.v b/proofs/compiler/slh_lowering_proof.v
index 841de3935..f8e793e15 100644
--- a/proofs/compiler/slh_lowering_proof.v
+++ b/proofs/compiler/slh_lowering_proof.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 
 Require Import
   expr
diff --git a/proofs/compiler/stack_alloc.v b/proofs/compiler/stack_alloc.v
index 7ce62145d..8ce00d6b5 100644
--- a/proofs/compiler/stack_alloc.v
+++ b/proofs/compiler/stack_alloc.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import strings word utils type var expr.
 Require Import compiler_util byteset.
diff --git a/proofs/compiler/stack_alloc_proof.v b/proofs/compiler/stack_alloc_proof.v
index 8b577e293..29b625f05 100644
--- a/proofs/compiler/stack_alloc_proof.v
+++ b/proofs/compiler/stack_alloc_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import psem psem_facts compiler_util low_memory.
 Require Export stack_alloc.
diff --git a/proofs/compiler/stack_alloc_proof_2.v b/proofs/compiler/stack_alloc_proof_2.v
index f71f52dc6..c07725dd2 100644
--- a/proofs/compiler/stack_alloc_proof_2.v
+++ b/proofs/compiler/stack_alloc_proof_2.v
@@ -3,7 +3,8 @@
 *)
 
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype fintype.
+From mathcomp Require Import div ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import psem psem_facts compiler_util.
 Require Export stack_alloc stack_alloc_proof.
diff --git a/proofs/compiler/stack_zeroization.v b/proofs/compiler/stack_zeroization.v
index c0c38118c..2e5fa921d 100644
--- a/proofs/compiler/stack_zeroization.v
+++ b/proofs/compiler/stack_zeroization.v
@@ -12,9 +12,7 @@ In export functions we set the [stk_max] field to a multiple of the size
 of a clearing step, so that the overwriting is done in an integer number of
 writes. *)
 
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import word_ssrZ.
 Require Import ZArith.
 
diff --git a/proofs/compiler/stack_zeroization_proof.v b/proofs/compiler/stack_zeroization_proof.v
index 662c215f1..911798ebb 100644
--- a/proofs/compiler/stack_zeroization_proof.v
+++ b/proofs/compiler/stack_zeroization_proof.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import ZArith.
 
diff --git a/proofs/compiler/tunneling.v b/proofs/compiler/tunneling.v
index 5125ff590..4790fa3d6 100644
--- a/proofs/compiler/tunneling.v
+++ b/proofs/compiler/tunneling.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import ZArith.
 
 Require Import Utf8.
diff --git a/proofs/compiler/tunneling_proof.v b/proofs/compiler/tunneling_proof.v
index 8a75d5320..0ae99e44d 100644
--- a/proofs/compiler/tunneling_proof.v
+++ b/proofs/compiler/tunneling_proof.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 Require Import ZArith.
 Require Import Utf8.
 
diff --git a/proofs/compiler/unionfind.v b/proofs/compiler/unionfind.v
index 4dd4401c0..5166f8cde 100644
--- a/proofs/compiler/unionfind.v
+++ b/proofs/compiler/unionfind.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 Require Import Utf8.
 Require Import expr label.
 
diff --git a/proofs/compiler/unionfind_proof.v b/proofs/compiler/unionfind_proof.v
index 66e32e09b..61f5c2ab8 100644
--- a/proofs/compiler/unionfind_proof.v
+++ b/proofs/compiler/unionfind_proof.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 Require Import Utf8.
 Require Import expr label.
 
diff --git a/proofs/compiler/unrolling.v b/proofs/compiler/unrolling.v
index 3171aa45e..f448552d1 100644
--- a/proofs/compiler/unrolling.v
+++ b/proofs/compiler/unrolling.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 Require Import ZArith expr compiler_util.
 
 Set Implicit Arguments.
diff --git a/proofs/compiler/unrolling_proof.v b/proofs/compiler/unrolling_proof.v
index 91e6fce4a..97fc16e79 100644
--- a/proofs/compiler/unrolling_proof.v
+++ b/proofs/compiler/unrolling_proof.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 Require Import ZArith psem compiler_util.
 Require Export unrolling.
 
diff --git a/proofs/compiler/x86.v b/proofs/compiler/x86.v
index 7481ea244..5619ad15c 100644
--- a/proofs/compiler/x86.v
+++ b/proofs/compiler/x86.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import sem_type arch_decl x86_decl x86_instr_decl.
 
 Set   Implicit Arguments.
diff --git a/proofs/compiler/x86_decl.v b/proofs/compiler/x86_decl.v
index a1ce6b10f..d70910505 100644
--- a/proofs/compiler/x86_decl.v
+++ b/proofs/compiler/x86_decl.v
@@ -1,5 +1,5 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice fintype.
 From mathcomp Require Import word_ssrZ.
 Require oseq.
 Require Import ZArith
diff --git a/proofs/compiler/x86_extra.v b/proofs/compiler/x86_extra.v
index aed15b162..3ed1f9ed2 100644
--- a/proofs/compiler/x86_extra.v
+++ b/proofs/compiler/x86_extra.v
@@ -1,6 +1,6 @@
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import Utf8.
 Require Import compiler_util.
diff --git a/proofs/compiler/x86_instr_decl.v b/proofs/compiler/x86_instr_decl.v
index e8c267a18..cc4c9e274 100644
--- a/proofs/compiler/x86_instr_decl.v
+++ b/proofs/compiler/x86_instr_decl.v
@@ -1,6 +1,6 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import word word_ssrZ.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype tuple.
+From mathcomp Require Import ssralg word word_ssrZ.
 Require Import utils strings word waes sem_type global oseq sopn.
 Import Utf8 Relation_Operators ZArith.
 
diff --git a/proofs/compiler/x86_lowering.v b/proofs/compiler/x86_lowering.v
index 9d29797a1..9f9316089 100644
--- a/proofs/compiler/x86_lowering.v
+++ b/proofs/compiler/x86_lowering.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import Utf8.
 Require Import
diff --git a/proofs/compiler/x86_lowering_proof.v b/proofs/compiler/x86_lowering_proof.v
index 355bdc670..cb8b04c18 100644
--- a/proofs/compiler/x86_lowering_proof.v
+++ b/proofs/compiler/x86_lowering_proof.v
@@ -2,8 +2,8 @@
 (* * Correctness proof of the lowering pass *)
 
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import word_ssrZ.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype order.
+From mathcomp Require Import ssralg ssrnum word_ssrZ.
 Require Import ZArith psem compiler_util lea_proof x86_instr_decl x86_extra.
 Require Import
   lowering
diff --git a/proofs/compiler/x86_params.v b/proofs/compiler/x86_params.v
index 3d80ddf1d..5acb27433 100644
--- a/proofs/compiler/x86_params.v
+++ b/proofs/compiler/x86_params.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 
 Require Import
diff --git a/proofs/compiler/x86_params_proof.v b/proofs/compiler/x86_params_proof.v
index d9a461a42..aa986053b 100644
--- a/proofs/compiler/x86_params_proof.v
+++ b/proofs/compiler/x86_params_proof.v
@@ -1,5 +1,5 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import word_ssrZ.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype finfun.
+From mathcomp Require Import ssralg word_ssrZ.
 
 Require Import
   arch_params_proof
diff --git a/proofs/compiler/x86_stack_zeroization.v b/proofs/compiler/x86_stack_zeroization.v
index 990957d11..90223a1d0 100644
--- a/proofs/compiler/x86_stack_zeroization.v
+++ b/proofs/compiler/x86_stack_zeroization.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
-
 Require Import
   expr
   fexpr
diff --git a/proofs/compiler/x86_stack_zeroization_proof.v b/proofs/compiler/x86_stack_zeroization_proof.v
index e6ba16290..a0f5d1d33 100644
--- a/proofs/compiler/x86_stack_zeroization_proof.v
+++ b/proofs/compiler/x86_stack_zeroization_proof.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import Lia.
 
diff --git a/proofs/lang/array.v b/proofs/lang/array.v
index f7c9970be..42023e1cd 100644
--- a/proofs/lang/array.v
+++ b/proofs/lang/array.v
@@ -1,5 +1,5 @@
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
-From mathcomp Require Import all_ssreflect.
 Require Import utils gen_map.
 
 Import ZArith.
diff --git a/proofs/lang/expr.v b/proofs/lang/expr.v
index 03844ace5..160455aa9 100644
--- a/proofs/lang/expr.v
+++ b/proofs/lang/expr.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype div ssralg.
 Require Import oseq.
 Require Export ZArith Setoid Morphisms.
 From mathcomp Require Import word_ssrZ.
diff --git a/proofs/lang/expr_facts.v b/proofs/lang/expr_facts.v
index 18c813dfe..8d2c5a34a 100644
--- a/proofs/lang/expr_facts.v
+++ b/proofs/lang/expr_facts.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 Require Import Utf8.
 Require Export expr.
 
diff --git a/proofs/lang/fexpr.v b/proofs/lang/fexpr.v
index b4c92ff5c..c335e5071 100644
--- a/proofs/lang/fexpr.v
+++ b/proofs/lang/fexpr.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 From Coq Require Import Utf8.
 Require Import expr.
 
diff --git a/proofs/lang/fexpr_facts.v b/proofs/lang/fexpr_facts.v
index 99b7ec4af..09ea9bd85 100644
--- a/proofs/lang/fexpr_facts.v
+++ b/proofs/lang/fexpr_facts.v
@@ -1,6 +1,6 @@
 From Coq Require Import Utf8.
 Require Import oseq.
-From mathcomp Require Import all_ssreflect ssralg.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 Require Import fexpr fexpr_sem.
 Require Import expr psem.
 
diff --git a/proofs/lang/fexpr_sem.v b/proofs/lang/fexpr_sem.v
index 08771e456..d1a06e61e 100644
--- a/proofs/lang/fexpr_sem.v
+++ b/proofs/lang/fexpr_sem.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssralg.
 Require Import fexpr.
 Require Import psem.
 
diff --git a/proofs/lang/flag_combination.v b/proofs/lang/flag_combination.v
index b40888970..73f4076ef 100644
--- a/proofs/lang/flag_combination.v
+++ b/proofs/lang/flag_combination.v
@@ -1,7 +1,3 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
-
 Require Import expr.
 
 Set Implicit Arguments.
diff --git a/proofs/lang/gen_map.v b/proofs/lang/gen_map.v
index d1e89077f..b2197fc2a 100644
--- a/proofs/lang/gen_map.v
+++ b/proofs/lang/gen_map.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 Require Import FMaps FMapAVL FSetAVL.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype.
 Require Import utils.
 
 Set Implicit Arguments.
diff --git a/proofs/lang/global.v b/proofs/lang/global.v
index 1ac88788a..d37602ac3 100644
--- a/proofs/lang/global.v
+++ b/proofs/lang/global.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import xseq.
 Require Export xseq ZArith strings word utils var type warray_.
diff --git a/proofs/lang/ident.v b/proofs/lang/ident.v
index 5feed3296..3cb9e9865 100644
--- a/proofs/lang/ident.v
+++ b/proofs/lang/ident.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import Sint63 strings utils gen_map tagged wsize.
 Require Import Utf8.
 
diff --git a/proofs/lang/linear.v b/proofs/lang/linear.v
index f737ca7b5..7e02d1b6e 100644
--- a/proofs/lang/linear.v
+++ b/proofs/lang/linear.v
@@ -1,6 +1,6 @@
 (* * Syntax of the linear language *)
 
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype ssralg.
 Require Import expr fexpr label sopn.
 
 Set Implicit Arguments.
diff --git a/proofs/lang/linear_facts.v b/proofs/lang/linear_facts.v
index 1a527b0ee..fbc8b193a 100644
--- a/proofs/lang/linear_facts.v
+++ b/proofs/lang/linear_facts.v
@@ -1,7 +1,5 @@
 From Coq Require Import Relations.
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 
 Require Import
   fexpr_facts
diff --git a/proofs/lang/linear_sem.v b/proofs/lang/linear_sem.v
index 99e8bca1e..7feaac91a 100644
--- a/proofs/lang/linear_sem.v
+++ b/proofs/lang/linear_sem.v
@@ -2,7 +2,7 @@
 
 (* ** Imports and settings *)
 
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat ssralg.
 Require Import ZArith Utf8.
         Import Relations.
 Require oseq.
diff --git a/proofs/lang/low_memory.v b/proofs/lang/low_memory.v
index 48d4668b5..62c76a48b 100644
--- a/proofs/lang/low_memory.v
+++ b/proofs/lang/low_memory.v
@@ -3,7 +3,7 @@
 From Coq Require Import RelationClasses.
 Require memory_example.
 
-Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import Lia.
 Import Utf8 ZArith.
diff --git a/proofs/lang/lowering_lemmas.v b/proofs/lang/lowering_lemmas.v
index ee2b957cf..96cafd027 100644
--- a/proofs/lang/lowering_lemmas.v
+++ b/proofs/lang/lowering_lemmas.v
@@ -1,6 +1,4 @@
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 
 Require Import
   expr
diff --git a/proofs/lang/memory_example.v b/proofs/lang/memory_example.v
index 560e052c7..2b6d8dd4a 100644
--- a/proofs/lang/memory_example.v
+++ b/proofs/lang/memory_example.v
@@ -24,7 +24,7 @@ We additionally maintain two invariants:
 Require memory_model array type.
 
 Import Utf8.
-Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype ssralg.
 Import ZArith Lia.
 Import word_ssrZ.
 Import type word utils gen_map.
diff --git a/proofs/lang/memory_model.v b/proofs/lang/memory_model.v
index 712b773c8..9cd995315 100644
--- a/proofs/lang/memory_model.v
+++ b/proofs/lang/memory_model.v
@@ -1,7 +1,7 @@
 (* ** Imports and settings *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import word_ssrZ.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq div eqtype.
+From mathcomp Require Import ssralg word_ssrZ.
 Require Import strings word utils.
 Import Utf8 ZArith Lia.
 Import ssrring.
diff --git a/proofs/lang/one_varmap.v b/proofs/lang/one_varmap.v
index b7dc1b66e..4ca47740b 100644
--- a/proofs/lang/one_varmap.v
+++ b/proofs/lang/one_varmap.v
@@ -3,7 +3,7 @@ This language is structured (as jasmin-source) and is used just before lineariza
 *)
 Require Import expr compiler_util.
 Import Utf8.
-Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/proofs/lang/psem.v b/proofs/lang/psem.v
index 84c578250..6ab7f2927 100644
--- a/proofs/lang/psem.v
+++ b/proofs/lang/psem.v
@@ -1,7 +1,7 @@
 (* * Jasmin semantics with “partial values”. *)
 
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 Require Import xseq.
 Require Export array type expr gen_map warray_ sem_type sem_op_typed values varmap expr_facts low_memory syscall_sem psem_defs.
 Require Export
diff --git a/proofs/lang/psem_defs.v b/proofs/lang/psem_defs.v
index dd41e2eaa..baba6b594 100644
--- a/proofs/lang/psem_defs.v
+++ b/proofs/lang/psem_defs.v
@@ -1,7 +1,7 @@
 (* * Jasmin semantics with “partial values”. *)
 
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 Require Import xseq.
 Require Export array type expr gen_map low_memory warray_ sem_type sem_op_typed values varmap low_memory syscall_sem.
 Require Export
diff --git a/proofs/lang/psem_facts.v b/proofs/lang/psem_facts.v
index b84f1070d..265d28526 100644
--- a/proofs/lang/psem_facts.v
+++ b/proofs/lang/psem_facts.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 Require Import psem.
 Import Utf8 Lia.
 Import Memory low_memory.
diff --git a/proofs/lang/psem_of_sem_proof.v b/proofs/lang/psem_of_sem_proof.v
index cb2df057b..623f8df12 100644
--- a/proofs/lang/psem_of_sem_proof.v
+++ b/proofs/lang/psem_of_sem_proof.v
@@ -1,6 +1,6 @@
 Require Import psem psem_facts.
 Import Utf8.
-Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/proofs/lang/pseudo_operator.v b/proofs/lang/pseudo_operator.v
index aaaaed67a..eabbed500 100644
--- a/proofs/lang/pseudo_operator.v
+++ b/proofs/lang/pseudo_operator.v
@@ -1,7 +1,5 @@
 From Coq Require Import ZArith.
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype.
 
 Require Import
   strings
diff --git a/proofs/lang/sem_one_varmap.v b/proofs/lang/sem_one_varmap.v
index 22f63514a..557135858 100644
--- a/proofs/lang/sem_one_varmap.v
+++ b/proofs/lang/sem_one_varmap.v
@@ -2,7 +2,7 @@
 *)
 Require psem one_varmap.
 Import Utf8.
-Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Export one_varmap.
 Import psem var.
 Import low_memory.
diff --git a/proofs/lang/sem_one_varmap_facts.v b/proofs/lang/sem_one_varmap_facts.v
index 66e22e907..9b8a4934c 100644
--- a/proofs/lang/sem_one_varmap_facts.v
+++ b/proofs/lang/sem_one_varmap_facts.v
@@ -2,7 +2,7 @@
 *)
 Require psem_facts sem_one_varmap.
 Import Utf8.
-Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Import low_memory.
 Import psem psem_facts sem_one_varmap.
 
diff --git a/proofs/lang/sem_op_typed.v b/proofs/lang/sem_op_typed.v
index 7c09bc805..bbadc59c8 100644
--- a/proofs/lang/sem_op_typed.v
+++ b/proofs/lang/sem_op_typed.v
@@ -1,5 +1,5 @@
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype div ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Export type expr sem_type.
 Require Export flag_combination.
diff --git a/proofs/lang/sem_type.v b/proofs/lang/sem_type.v
index 559353016..97f71335a 100644
--- a/proofs/lang/sem_type.v
+++ b/proofs/lang/sem_type.v
@@ -1,7 +1,7 @@
 (* * Syntax and semantics of the Jasmin source language *)
 
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import xseq.
 Require Export strings warray_.
diff --git a/proofs/lang/slh_ops.v b/proofs/lang/slh_ops.v
index 9842e7067..68b4cf94d 100644
--- a/proofs/lang/slh_ops.v
+++ b/proofs/lang/slh_ops.v
@@ -1,7 +1,5 @@
 From HB Require Import structures.
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat div eqtype ssralg.
 
 Require Import
   sem_type
diff --git a/proofs/lang/sopn.v b/proofs/lang/sopn.v
index f4c9a0cfe..b9ac2ed58 100644
--- a/proofs/lang/sopn.v
+++ b/proofs/lang/sopn.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype ssralg.
 
 Require Import
   pseudo_operator
diff --git a/proofs/lang/stack_zero_strategy.v b/proofs/lang/stack_zero_strategy.v
index f57a614bf..2a60d623d 100644
--- a/proofs/lang/stack_zero_strategy.v
+++ b/proofs/lang/stack_zero_strategy.v
@@ -12,9 +12,7 @@ circular dependency. *)
 
 From HB Require Import structures.
 
-From mathcomp Require Import
-  all_ssreflect
-  ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype fintype.
 Require Import utils.
 
 Set Implicit Arguments.
diff --git a/proofs/lang/strings.v b/proofs/lang/strings.v
index 248120279..9c2ce31bc 100644
--- a/proofs/lang/strings.v
+++ b/proofs/lang/strings.v
@@ -1,7 +1,7 @@
 Require Import ZArith.
 Require Export String.
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice.
 Require Import utils gen_map.
 
 Set Implicit Arguments.
diff --git a/proofs/lang/syscall.v b/proofs/lang/syscall.v
index 687deb055..14faeb1e5 100644
--- a/proofs/lang/syscall.v
+++ b/proofs/lang/syscall.v
@@ -1,5 +1,5 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype ssralg.
 From Coq Require Import PArith ZArith.
 Require Import
   word
diff --git a/proofs/lang/syscall_sem.v b/proofs/lang/syscall_sem.v
index 6a843b0e5..6fbdd3b71 100644
--- a/proofs/lang/syscall_sem.v
+++ b/proofs/lang/syscall_sem.v
@@ -1,7 +1,7 @@
 (* * Jasmin semantics with “partial values”. *)
 
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq ssralg.
 Require Import ZArith.
 Require Export utils syscall wsize word type low_memory sem_type values.
 Import Utf8.
diff --git a/proofs/lang/tagged.v b/proofs/lang/tagged.v
index aafe254e3..5d2d94b82 100644
--- a/proofs/lang/tagged.v
+++ b/proofs/lang/tagged.v
@@ -1,5 +1,5 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import PrimInt63 Sint63 utils gen_map.
 
 Set Implicit Arguments.
diff --git a/proofs/lang/type.v b/proofs/lang/type.v
index 96dc58745..492701fc9 100644
--- a/proofs/lang/type.v
+++ b/proofs/lang/type.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import ZArith gen_map utils strings.
 Require Export wsize.
 Import Utf8.
diff --git a/proofs/lang/utils.v b/proofs/lang/utils.v
index a1a44553d..99ac993d6 100644
--- a/proofs/lang/utils.v
+++ b/proofs/lang/utils.v
@@ -1,6 +1,7 @@
 (* ** Imports and settings *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
+From mathcomp Require Import fintype finfun.
 From Coq.Unicode Require Import Utf8.
 From Coq Require Import ZArith Zwf Setoid Morphisms CMorphisms CRelationClasses.
 Require Import xseq oseq.
diff --git a/proofs/lang/values.v b/proofs/lang/values.v
index 3b815f779..821e44280 100644
--- a/proofs/lang/values.v
+++ b/proofs/lang/values.v
@@ -1,7 +1,7 @@
 (* * Syntax and semantics of the Jasmin source language *)
 
 (* ** Imports and settings *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import xseq.
 Require Export warray_ word sem_type.
diff --git a/proofs/lang/var.v b/proofs/lang/var.v
index 93fbd8d43..b3b36bf29 100644
--- a/proofs/lang/var.v
+++ b/proofs/lang/var.v
@@ -1,7 +1,7 @@
 (* ** Imports and settings *)
 Require Import Setoid Morphisms.
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype.
 Require Import strings utils gen_map type ident tagged.
 Require Import Utf8.
 
diff --git a/proofs/lang/varmap.v b/proofs/lang/varmap.v
index d0b19d9bc..a17741b9a 100644
--- a/proofs/lang/varmap.v
+++ b/proofs/lang/varmap.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype ssralg.
 Require Import ZArith Setoid Morphisms.
 Require Export var type values.
 Import Utf8 ssrbool.
diff --git a/proofs/lang/waes.v b/proofs/lang/waes.v
index 2b8141fe4..354aa73b2 100644
--- a/proofs/lang/waes.v
+++ b/proofs/lang/waes.v
@@ -3,7 +3,7 @@
 
 (* ** Imports and settings *)
 
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq ssralg.
 From mathcomp Require Import word_ssrZ word.
 Require Import word.
 Require Import ZArith utils.
diff --git a/proofs/lang/warray_.v b/proofs/lang/warray_.v
index a71632d4f..9b1b32b87 100644
--- a/proofs/lang/warray_.v
+++ b/proofs/lang/warray_.v
@@ -3,7 +3,7 @@
 (* ** Imports and settings *)
 Require Export ZArith Setoid Morphisms.
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype div ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import xseq.
 Require Export utils array gen_map type word memory_model.
diff --git a/proofs/lang/word.v b/proofs/lang/word.v
index fa017fff2..2df1217c8 100644
--- a/proofs/lang/word.v
+++ b/proofs/lang/word.v
@@ -2,8 +2,8 @@
 
 (* ** Imports and settings *)
 
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import word_ssrZ word.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype tuple.
+From mathcomp Require Import div fintype order ssralg ssrnum word_ssrZ word.
 Require Import ssrring.
 Require Zquot.
 Require Import ZArith utils.
diff --git a/proofs/lang/wsize.v b/proofs/lang/wsize.v
index 9262f175b..3b59490c8 100644
--- a/proofs/lang/wsize.v
+++ b/proofs/lang/wsize.v
@@ -3,7 +3,7 @@
 (* ** Imports and settings *)
 
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype fintype.
 Require Import strings ZArith utils.
 Import Utf8.
 Import word_ssrZ.
diff --git a/proofs/ssrmisc/oseq.v b/proofs/ssrmisc/oseq.v
index 8ceca8b10..2a2a33107 100644
--- a/proofs/ssrmisc/oseq.v
+++ b/proofs/ssrmisc/oseq.v
@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/proofs/ssrmisc/seq_extra.v b/proofs/ssrmisc/seq_extra.v
index 930297c98..c9a559a9a 100644
--- a/proofs/ssrmisc/seq_extra.v
+++ b/proofs/ssrmisc/seq_extra.v
@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq.
 Require Import Utf8 oseq utils.
 
 Set Implicit Arguments.