adapting solvable to 8.5

1 files changed, 7 insertions, 2 deletions

diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v
index e097765..90ba407 100644
--- a/mathcomp/solvable/hall.v
+++ b/mathcomp/solvable/hall.v
@@ -1,6 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype finset.
-Require Import prime fingroup morphism automorphism quotient action gproduct.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype finset bigop prime.
+From mathcomp.fingroup
+Require Import fingroup morphism automorphism quotient action gproduct.
 Require Import commutator center pgroup finmodule nilpotent sylow.
 Require Import abelian maximal.