Minimize imports

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

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.
 

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

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

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.

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

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.

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.

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.

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.
 

proofs/compiler/arch_params.v

@@ -1,4 +1,3 @@
-From mathcomp Require Import all_ssreflect ssralg ssrnum.
 Require Import
   compiler_util
   expr.

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

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.

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

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

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

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

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

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

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.

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

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

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

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

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

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.

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

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.
 

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

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.

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.

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.

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.

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.

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.
 

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.
 

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

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.

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.

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.
 

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.

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.

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.

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.

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.

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.

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.
 

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.

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.

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.
 

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.