From 999e5fdc1d11285949b3c3d2a4a582d7bf2ba8e3 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 9 Apr 2015 14:47:46 +0200
Subject: adapting solvable to 8.5

---
 mathcomp/solvable/finmodule.v | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'mathcomp/solvable/finmodule.v')

diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v
index e2eae84..dd84def 100644
--- a/mathcomp/solvable/finmodule.v
+++ b/mathcomp/solvable/finmodule.v
@@ -1,7 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
-Require Import fintype bigop ssralg finset fingroup morphism perm.
-Require Import finalg action gproduct commutator cyclic.
+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 bigop prime finset.
+From mathcomp.fingroup
+Require Import fingroup morphism perm action gproduct.
+From mathcomp.algebra
+Require Import ssralg finalg cyclic.
+Require Import commutator.
 
 (******************************************************************************)
 (*  This file regroups constructions and results that are based on the most   *)
-- 
cgit v1.2.3