diff options
Diffstat (limited to 'mathcomp')
| -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 |