Change Implicit Arguments to Arguments in fingroup

7 files changed, 88 insertions, 88 deletions

diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index ecfa6ea..6478c81 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -287,7 +287,7 @@ Variables (aT : finGroupType) (D : {set aT}) (rT : finType) (to : action D rT).
 Implicit Types (a : aT) (x y : rT) (A B : {set aT}) (S T : {set rT}).
 
 Lemma act_inj : left_injective to. Proof. by case: to => ? []. Qed.
-Implicit Arguments act_inj [].
+Arguments act_inj : clear implicits.
 
 Lemma actMin x : {in D &, act_morph to x}.
 Proof. by case: to => ? []. Qed.
@@ -486,17 +486,17 @@ End RawAction.
 
 (* Warning: this directive depends on names of bound variables in the *)
 (* definition of injective, in ssrfun.v.                              *)
-Implicit Arguments act_inj [[aT] [D] [rT] x1 x2].
+Arguments act_inj {aT D rT} to _ [x1 x2].
 
 Notation "to ^*" := (set_action to) : action_scope.
 
-Implicit Arguments orbitP [aT D rT to A x y].
-Implicit Arguments afixP [aT D rT to A x].
-Implicit Arguments afix1P [aT D rT to a x].
+Arguments orbitP [aT D rT to A x y].
+Arguments afixP [aT D rT to A x].
+Arguments afix1P [aT D rT to a x].
 Prenex Implicits orbitP afixP afix1P.
 
-Implicit Arguments reindex_astabs [aT D rT vT idx op S F].
-Implicit Arguments reindex_acts [aT D rT vT idx op S A a F].
+Arguments reindex_astabs [aT D rT] to [vT idx op S] a [F].
+Arguments reindex_acts [aT D rT] to [vT idx op S A a F].
 
 Section PartialAction.
 (* Lemmas that require a (partial) group domain. *)
@@ -879,9 +879,9 @@ End PartialAction.
 
 Arguments Scope orbit_transversal
   [_ group_scope _ action_scope group_scope group_scope].
-Implicit Arguments orbit_in_eqP [aT D rT to G x y].
-Implicit Arguments orbit1P [aT D rT to G x].
-Implicit Arguments contra_orbit [aT D rT x y].
+Arguments orbit_in_eqP [aT D rT to G x y].
+Arguments orbit1P [aT D rT to G x].
+Arguments contra_orbit [aT D rT] to G [x y].
 Prenex Implicits orbit_in_eqP orbit1P.
 
 Notation "''C' ( S | to )" := (astab_group to S) : Group_scope.
@@ -1008,7 +1008,7 @@ Proof.
 apply: (iffP idP) => [nSA x|nSA]; first exact: acts_act.
 by apply/subsetP=> a Aa; rewrite !inE; apply/subsetP=> x; rewrite inE nSA.
 Qed.
-Implicit Arguments actsP [A S].
+Arguments actsP [A S].
 
 Lemma setact_orbit A x b : to^* (orbit to A x) b = orbit to (A :^ b) (to x b).
 Proof.
@@ -1137,13 +1137,13 @@ Qed.
 
 End TotalActions.
 
-Implicit Arguments astabP [aT rT to S a].
-Implicit Arguments orbit_eqP [aT rT to G x y].
-Implicit Arguments astab1P [aT rT to x a].
-Implicit Arguments astabsP [aT rT to S a].
-Implicit Arguments atransP [aT rT to G S].
-Implicit Arguments actsP [aT rT to A S].
-Implicit Arguments faithfulP [aT rT to A S].
+Arguments astabP [aT rT to S a].
+Arguments orbit_eqP [aT rT to G x y].
+Arguments astab1P [aT rT to x a].
+Arguments astabsP [aT rT to S a].
+Arguments atransP [aT rT to G S].
+Arguments actsP [aT rT to A S].
+Arguments faithfulP [aT rT to A S].
 Prenex Implicits astabP orbit_eqP astab1P astabsP atransP actsP faithfulP.
 
 Section Restrict.
@@ -1637,7 +1637,7 @@ Proof. by apply/permP=> x; rewrite permE. Qed.
 
 End PermAction.
 
-Implicit Arguments perm_act1P [rT a].
+Arguments perm_act1P [rT a].
 Prenex Implicits perm_act1P.
 
 Notation "'P" := (perm_action _) (at level 8) : action_scope.
diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index 8813b45..e727aba 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.v
@@ -198,7 +198,7 @@ Qed.
 
 End MakeAut.
 
-Implicit Arguments morphim_fixP [gT G f].
+Arguments morphim_fixP [gT G f].
 Prenex Implicits aut morphim_fixP.
 
 Section AutIsom.
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index dd57af4..5afc3c7 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -493,7 +493,7 @@ Qed.
 End PreGroupIdentities.
 
 Hint Resolve commute1.
-Implicit Arguments invg_inj [T].
+Arguments invg_inj [T].
 Prenex Implicits commute invgK invg_inj.
 
 Section GroupIdentities.
@@ -641,11 +641,11 @@ Ltac gsimpl := autorewrite with gsimpl; try done.
 Definition gsimp := (mulg1 , mul1g, (invg1, @invgK), (mulgV, mulVg)).
 Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))).
 
-Implicit Arguments mulgI [T].
-Implicit Arguments mulIg [T].
-Implicit Arguments conjg_inj [T].
-Implicit Arguments commgP [T x y].
-Implicit Arguments conjg_fixP [T x y].
+Arguments mulgI [T].
+Arguments mulIg [T].
+Arguments conjg_inj [T].
+Arguments commgP [T x y].
+Arguments conjg_fixP [T x y].
 Prenex Implicits conjg_fixP commgP.
 
 Section Repr.
@@ -672,7 +672,7 @@ Proof. by rewrite /repr; case: pickP => [x|_]; rewrite !inE. Qed.
 
 End Repr.
 
-Implicit Arguments mem_repr [gT A].
+Arguments mem_repr [gT A].
 
 Section BaseSetMulDef.
 (* We only assume a baseFinGroupType to allow this construct to be iterated. *)
@@ -946,9 +946,9 @@ Proof. by apply/setP=> y; rewrite !inE inv_eq //; apply: invgK. Qed.
 
 End BaseSetMulProp.
 
-Implicit Arguments set1gP [gT x].
-Implicit Arguments mulsgP [gT A B x].
-Implicit Arguments prodsgP [gT I P A x].
+Arguments set1gP [gT x].
+Arguments mulsgP [gT A B x].
+Arguments prodsgP [gT I P A x].
 
 Section GroupSetMulProp.
 (* Constructs that need a finGroupType *)
@@ -1304,11 +1304,11 @@ Definition order x := #|cycle x|.
 
 End GroupSetMulProp.
 
-Implicit Arguments lcosetP [gT A x y].
-Implicit Arguments lcosetsP [gT A B C].
-Implicit Arguments rcosetP [gT A x y].
-Implicit Arguments rcosetsP [gT A B C].
-Implicit Arguments group_setP [gT A].
+Arguments lcosetP [gT A x y].
+Arguments lcosetsP [gT A B C].
+Arguments rcosetP [gT A x y].
+Arguments rcosetsP [gT A B C].
+Arguments group_setP [gT A].
 Prenex Implicits group_set mulsgP set1gP.
 Prenex Implicits lcosetP lcosetsP rcosetP rcosetsP group_setP.
 
@@ -1858,15 +1858,15 @@ Notation "[ 'subg' G ]" := [set: subg_of G]%G : Group_scope.
 Prenex Implicits subg sgval subg_of.
 Bind Scope group_scope with subg_of.
 
-Implicit Arguments trivgP [gT G].
-Implicit Arguments trivGP [gT G].
-Implicit Arguments lcoset_eqP [gT G x y].
-Implicit Arguments rcoset_eqP [gT G x y].
-Implicit Arguments mulGidPl [gT G H].
-Implicit Arguments mulGidPr [gT G H].
-Implicit Arguments comm_group_setP [gT G H].
-Implicit Arguments class_eqP [gT G x y].
-Implicit Arguments repr_classesP [gT G xG].
+Arguments trivgP [gT G].
+Arguments trivGP [gT G].
+Arguments lcoset_eqP [gT G x y].
+Arguments rcoset_eqP [gT G x y].
+Arguments mulGidPl [gT G H].
+Arguments mulGidPr [gT G H].
+Arguments comm_group_setP [gT G H].
+Arguments class_eqP [gT G x y].
+Arguments repr_classesP [gT G xG].
 Prenex Implicits trivgP trivGP lcoset_eqP rcoset_eqP comm_group_setP class_eqP.
 
 Section GroupInter.
@@ -2396,11 +2396,11 @@ Qed.
 
 End GeneratedGroup.
 
-Implicit Arguments gen_prodgP [gT A x].
-Implicit Arguments joing_idPl [gT G A].
-Implicit Arguments joing_idPr [gT A G].
-Implicit Arguments mulGsubP [gT K H G].
-Implicit Arguments joing_subP [gT A B G].
+Arguments gen_prodgP [gT A x].
+Arguments joing_idPl [gT G A].
+Arguments joing_idPr [gT A G].
+Arguments mulGsubP [gT K H G].
+Arguments joing_subP [gT A B G].
 
 Section Cycles.
 
@@ -2524,7 +2524,7 @@ Proof.
 suffices ->: (x \in 'N(A)) = (A :^ x == A) by apply: eqP.
 by rewrite eqEcard cardJg leqnn andbT inE.
 Qed.
-Implicit Arguments normP [x A].
+Arguments normP [x A].
 
 Lemma group_set_normaliser A : group_set 'N(A).
 Proof.
@@ -2539,7 +2539,7 @@ Proof.
 apply: (iffP subsetP) => nBA x Ax; last by rewrite inE nBA //.
 by apply/normP; apply: nBA.
 Qed.
-Implicit Arguments normsP [A B].
+Arguments normsP [A B].
 
 Lemma memJ_norm x y A : x \in 'N(A) -> (y ^ x \in A) = (y \in A).
 Proof. by move=> Nx; rewrite -{1}(normP Nx) memJ_conjg. Qed.
@@ -2987,13 +2987,13 @@ End SubAbelian.
 
 End Normaliser.
 
-Implicit Arguments normP [gT x A].
-Implicit Arguments centP [gT x A].
-Implicit Arguments normsP [gT A B].
-Implicit Arguments cent1P [gT x y].
-Implicit Arguments normalP [gT A B].
-Implicit Arguments centsP [gT A B].
-Implicit Arguments commG1P [gT A B].
+Arguments normP [gT x A].
+Arguments centP [gT A x].
+Arguments normsP [gT A B].
+Arguments cent1P [gT x y].
+Arguments normalP [gT A B].
+Arguments centsP [gT A B].
+Arguments commG1P [gT A B].
 
 Prenex Implicits normP normsP cent1P normalP centP centsP commG1P.
 
@@ -3091,6 +3091,6 @@ Notation "[ 'min' A 'of' G | gP & gQ ]" :=
   [min A of G | gP && gQ] : group_scope.
 Notation "[ 'min' G | gP & gQ ]" := [min G | gP && gQ] : group_scope.
 
-Implicit Arguments mingroupP [gT gP G].
-Implicit Arguments maxgroupP [gT gP G].
+Arguments mingroupP [gT gP G].
+Arguments maxgroupP [gT gP G].
 Prenex Implicits mingroupP maxgroupP.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index cd129f2..dc16021 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -96,10 +96,10 @@ Arguments Scope complements_to_in [_ group_scope group_scope].
 Arguments Scope splits_over [_ group_scope group_scope].
 Arguments Scope remgr [_ group_scope group_scope group_scope].
 Arguments Scope divgr [_ group_scope group_scope group_scope].
-Implicit Arguments partial_product [].
-Implicit Arguments semidirect_product [].
-Implicit Arguments central_product [].
-Implicit Arguments direct_product [].
+Arguments partial_product : clear implicits.
+Arguments semidirect_product : clear implicits.
+Arguments central_product : clear implicits.
+Arguments direct_product : clear implicits.
 Notation pprod := (partial_product _).
 Notation sdprod := (semidirect_product _).
 Notation cprod := (central_product _).
@@ -870,11 +870,11 @@ Qed.
 
 End InternalProd.
 
-Implicit Arguments complP [gT H A B].
-Implicit Arguments splitsP [gT A B].
-Implicit Arguments sdprod_normal_complP [gT K H G].
-Implicit Arguments dprodYP [gT K H].
-Implicit Arguments bigdprodYP [gT I P F].
+Arguments complP [gT H A B].
+Arguments splitsP [gT B A].
+Arguments sdprod_normal_complP [gT G K H].
+Arguments dprodYP [gT K H].
+Arguments bigdprodYP [gT I P F].
 
 Section MorphimInternalProd.
 
@@ -1703,5 +1703,5 @@ Qed.
 
 End DirprodIsom.
 
-Implicit Arguments mulgmP [gT H1 H2 G].
+Arguments mulgmP [gT H1 H2 G].
 Prenex Implicits mulgm mulgmP.
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index 2a70706..315358b 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -118,8 +118,8 @@ Notation "[ 'morphism' D 'of' f ]" :=
 Notation "[ 'morphism' 'of' f ]" := (clone_morphism (@Morphism _ _ _ f))
    (at level 0, format "[ 'morphism'  'of'  f ]") : form_scope.
 
-Implicit Arguments morphimP [aT rT D A f y].
-Implicit Arguments morphpreP [aT rT D R f x].
+Arguments morphimP [aT rT D A y f].
+Arguments morphpreP [aT rT D R x f].
 Prenex Implicits morphimP morphpreP.
 
 (* Domain, image, preimage, kernel, using phantom types to infer the domain. *)
@@ -873,7 +873,7 @@ Notation "f @* G" := (morphim_group (MorPhantom f) G) : Group_scope.
 Notation "f @*^-1 M" := (morphpre_group (MorPhantom f) M) : Group_scope.
 Notation "f @: D" := (morph_dom_group f D) : Group_scope.
 
-Implicit Arguments injmP [aT rT D f].
+Arguments injmP [aT rT D f].
 
 Section IdentityMorphism.
 
@@ -969,8 +969,8 @@ End RestrictedMorphism.
 
 Arguments Scope restrm [_ _ group_scope group_scope _ group_scope].
 Prenex Implicits restrm.
-Implicit Arguments restrmP [aT rT D A].
-Implicit Arguments domP [aT rT D A].
+Arguments restrmP [aT rT A D].
+Arguments domP [aT rT A D].
 
 Section TrivMorphism.
 
@@ -995,7 +995,7 @@ Proof. by apply/setIidPl/subsetP=> x _; rewrite !inE /=. Qed.
 End TrivMorphism.
 
 Arguments Scope trivm [_ _ group_scope group_scope].
-Implicit Arguments trivm [[aT] [rT]].
+Arguments trivm {aT rT}.
 
 (* The composition of two morphisms is a Canonical morphism instance. *)
 Section MorphismComposition.
@@ -1259,7 +1259,7 @@ End Defs.
 
 Infix "\isog" := isog.
 
-Implicit Arguments isom_isog [A B D].
+Arguments isom_isog [A B D].
 
 (* The real reflection properties only hold for true groups and morphisms. *)
 
@@ -1330,11 +1330,11 @@ Arguments Scope morphic [_ _ group_scope _].
 Arguments Scope misom [_ _ group_scope group_scope _].
 Arguments Scope isog [_ _ group_scope group_scope].
 
-Implicit Arguments morphicP [aT rT A f].
-Implicit Arguments misomP [aT rT A B f].
-Implicit Arguments isom_isog [aT rT A B D].
-Implicit Arguments isomP [aT rT G H f].
-Implicit Arguments isogP [aT rT G H].
+Arguments morphicP [aT rT A f].
+Arguments misomP [aT rT A B f].
+Arguments isom_isog [aT rT A B D].
+Arguments isomP [aT rT G H f].
+Arguments isogP [aT rT G H].
 Prenex Implicits morphic morphicP morphm isom isog isomP misomP isogP.
 Notation "x \isog y":= (isog x y).
 
@@ -1483,7 +1483,7 @@ Arguments Scope homg [_ _ group_scope group_scope].
 Notation "G \homg H" := (homg G H)
   (at level 70, no associativity) : group_scope.
 
-Implicit Arguments homgP [rT aT C D].
+Arguments homgP [rT aT C D].
 
 (* Isomorphism between a group and its subtype. *)
 
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 6d9abdc..bbf4363 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -128,7 +128,7 @@ Proof. by move=> x; rewrite -pvalE [@perm]unlock ffunE. Qed.
 Lemma perm_inj s : injective s.
 Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed.
 
-Implicit Arguments perm_inj [].
+Arguments perm_inj : clear implicits.
 Hint Resolve perm_inj.
 
 Lemma perm_onto s : codom s =i predT.
@@ -461,7 +461,7 @@ Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y).
 Proof. by rewrite -[_ y]mulg1 odd_mul_tperm odd_perm1 addbF. Qed.
 
 Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT].
-Implicit Arguments dpair [eT].
+Arguments dpair [eT].
 
 Lemma prod_tpermP s :
   {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.
@@ -503,7 +503,7 @@ Proof. by rewrite !odd_permM odd_permV addbC addbK. Qed.
 End PermutationParity.
 
 Coercion odd_perm : perm_type >-> bool.
-Implicit Arguments dpair [eT].
+Arguments dpair [eT].
 Prenex Implicits pcycle dpair pcycles aperm.
 
 Section LiftPerm.
diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index 242b4b7..99d1aef 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.v
@@ -751,8 +751,8 @@ Qed.
 
 End EqIso.
 
-Implicit Arguments qisom_inj [gT G H].
-Implicit Arguments morphim_qisom_inj [gT G H].
+Arguments qisom_inj [gT G H].
+Arguments morphim_qisom_inj [gT G H].
 
 Section FirstIsomorphism.