aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/fingroup/all_fingroup.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/fingroup/all_fingroup.v')
-rw-r--r--mathcomp/fingroup/all_fingroup.v9
1 files changed, 9 insertions, 0 deletions
diff --git a/mathcomp/fingroup/all_fingroup.v b/mathcomp/fingroup/all_fingroup.v
new file mode 100644
index 0000000..903da3c
--- /dev/null
+++ b/mathcomp/fingroup/all_fingroup.v
@@ -0,0 +1,9 @@
+Require Export action.
+Require Export automorphism.
+Require Export fingroup.
+Require Export gproduct.
+Require Export morphism.
+Require Export perm.
+Require Export presentation.
+Require Export quotient.
+