From cef1a8eadcdef812ce9ee2738cb294644fafbfab Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 21 Feb 2018 23:43:44 -0800
Subject: Change Implicit Arguments to Arguments in solvable

---
 mathcomp/solvable/burnside_app.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/solvable/burnside_app.v')

diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v
index d9010d5..1c804cc 100644
--- a/mathcomp/solvable/burnside_app.v
+++ b/mathcomp/solvable/burnside_app.v
@@ -26,7 +26,7 @@ rewrite big_uniq // -(card_uniqP Us) (eq_card sG) -Frobenius_Cauchy.
 by apply/actsP=> ? _ ?; rewrite !inE.
 Qed.
 
-Implicit Arguments burnside_formula [gT].
+Arguments burnside_formula [gT].
 
 Section colouring.
 
-- 
cgit v1.2.3