packaging for v8.5

1 files changed, 7 insertions, 3 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index ecf5801..e67008d 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1,7 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import finfun bigop prime binomial ssralg finset fingroup finalg.
-Require Import perm zmodp.
+(*v8.5 From mathcomp.ssreflect *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+(*v8.5 From mathcomp.discrete *)
+Require Import  div choice fintype finfun bigop prime binomial finset.
+(*v8.5 From mathcomp.fingroup *)
+Require Import fingroup perm.
+Require Import ssralg finalg zmodp.
 
 (******************************************************************************)
 (* Basic concrete linear algebra : definition of type for matrices, and all   *)