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/frobenius.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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

diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v
index da65950..3416587 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -246,7 +246,7 @@ have Gg: g \in G by rewrite groupMl ?groupV.
 rewrite -conjIg (inj_eq (act_inj 'Js x)) (eq_sym A) (sameP eqP normP).
 by rewrite -cards_eq0 cardJg cards_eq0 setI_eq0 => /tiAG/(subsetP nAL)->.
 Qed.
-Implicit Arguments normedTI_P [A G L].
+Arguments normedTI_P [A G L].
 
 Lemma normedTI_memJ_P A G L :
   reflect [/\ A != set0, L \subset G
@@ -622,9 +622,9 @@ Qed.
 
 End FrobeniusBasics.
 
-Implicit Arguments normedTI_P [gT A G L].
-Implicit Arguments normedTI_memJ_P [gT A G L].
-Implicit Arguments Frobenius_kerP [gT G K].
+Arguments normedTI_P [gT A G L].
+Arguments normedTI_memJ_P [gT A G L].
+Arguments Frobenius_kerP [gT G K].
 
 Lemma Frobenius_coprime_quotient (gT : finGroupType) (G K H N : {group gT}) :
     K ><| H = G -> N <| G -> coprime #|K| #|H| /\ H :!=: 1%g ->
-- 
cgit v1.2.3