diff options
Diffstat (limited to 'mathcomp/algebra/finalg.v')
| -rw-r--r-- | mathcomp/algebra/finalg.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index b903577..d364fc9 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -1,6 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype. -Require Import ssralg finset fingroup morphism perm action. +(*v8.5 From mathcomp.ssreflect *) +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +(*v8.5 From mathcomp.discrete *) +Require Import choice fintype finset. +(*v8.5 From mathcomp.fingroup *) +Require Import fingroup morphism perm action. +Require Import ssralg. (*****************************************************************************) (* This file clones the entire ssralg hierachy for finite types; this allows *) |