diff options
| author | Enrico Tassi | 2020-09-14 15:11:14 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-09-14 18:55:29 +0200 |
| commit | 38b28c7d9756da7d346a1866a4ce712b1c3472af (patch) | |
| tree | c185403def5278aed62de33ad2da3b2ac0deeb52 /mathcomp/test_suite | |
| parent | 755068fd34f0fa1e918123c4859aef2e89bedfca (diff) | |
don't use all.v in output.v
Diffstat (limited to 'mathcomp/test_suite')
| -rw-r--r-- | mathcomp/test_suite/output.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/mathcomp/test_suite/output.v b/mathcomp/test_suite/output.v index 7e9def3..b0b0996 100644 --- a/mathcomp/test_suite/output.v +++ b/mathcomp/test_suite/output.v @@ -1,4 +1,10 @@ -From mathcomp Require Import all. +From mathcomp Require Import + all_ssreflect + all_algebra + all_field + all_character + all_fingroup + all_solvable. Open Scope group_scope. Check @cyclic_pgroup_Aut_structure.
\ No newline at end of file |