diff options
| author | Cyril Cohen | 2015-04-09 14:47:46 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2015-04-09 15:47:46 +0200 |
| commit | 999e5fdc1d11285949b3c3d2a4a582d7bf2ba8e3 (patch) | |
| tree | 148651f8d47d896af6801c0a0586ee2b3fb9aa34 /mathcomp/solvable/gfunctor.v | |
| parent | c8b1f9899665886b7bd0c7a25237d8e99afcced7 (diff) | |
adapting solvable to 8.5
Diffstat (limited to 'mathcomp/solvable/gfunctor.v')
| -rw-r--r-- | mathcomp/solvable/gfunctor.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index a338999..25295ff 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.v @@ -1,5 +1,10 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop finset. +Require Import mathcomp.ssreflect.ssreflect. +From mathcomp.ssreflect +Require Import ssreflect ssrbool ssrfun eqtype ssrnat. +From mathcomp.discrete +Require Import fintype bigop finset. +From mathcomp.fingroup Require Import fingroup morphism automorphism quotient gproduct. (******************************************************************************) |