From f049e51c39077a025907ea87c08178dad1841801 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Tue, 20 Nov 2018 17:51:11 +0100
Subject: Merge Arguments and Prenex Implicits

See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
---
 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 98657b4..f7edfc9 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -244,7 +244,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.
-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
@@ -620,9 +620,9 @@ Qed.
 
 End FrobeniusBasics.
 
-Arguments normedTI_P [gT A G L].
-Arguments normedTI_memJ_P [gT A G L].
-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