From 38b28c7d9756da7d346a1866a4ce712b1c3472af Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 14 Sep 2020 15:11:14 +0200
Subject: don't use all.v in output.v

---
 mathcomp/test_suite/output.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

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
-- 
cgit v1.2.3