Merge pull request #249 from anton-trunov/prenex-implicits

Merge Arguments and Prenex Implicits

7 files changed, 78 insertions, 92 deletions

diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index 5c5dcdc..ffea847 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -488,10 +488,9 @@ Arguments act_inj {aT D rT} to _ [x1 x2].
 
 Notation "to ^*" := (set_action to) : action_scope.
 
-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.
+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}.
 
 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].
@@ -876,10 +875,9 @@ Qed.
 End PartialAction.
 
 Arguments orbit_transversal _ _%g _ _%act _%g _%g.
-Arguments orbit_in_eqP [aT D rT to G x y].
-Arguments orbit1P [aT D rT to G x].
+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.
 Notation "''C_' A ( S | to )" := (setI_group A 'C(S | to)) : Group_scope.
@@ -1005,7 +1003,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.
-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.
@@ -1134,14 +1132,13 @@ Qed.
 
 End TotalActions.
 
-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.
+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}.
 
 Section Restrict.
 
@@ -1634,8 +1631,7 @@ Proof. by apply/permP=> x; rewrite permE. Qed.
 
 End PermAction.
 
-Arguments perm_act1P [rT a].
-Prenex Implicits perm_act1P.
+Arguments perm_act1P {rT a}.
 
 Notation "'P" := (perm_action _) (at level 8) : action_scope.
 
diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index b1c9d94..320331c 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.v
@@ -198,8 +198,8 @@ Qed.
 
 End MakeAut.
 
-Arguments morphim_fixP [gT G f].
-Prenex Implicits aut morphim_fixP.
+Arguments morphim_fixP {gT G f}.
+Prenex Implicits aut.
 
 Section AutIsom.
 
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 959eea1..1165a33 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -493,8 +493,8 @@ Qed.
 End PreGroupIdentities.
 
 Hint Resolve commute1.
-Arguments invg_inj [T].
-Prenex Implicits commute invgK invg_inj.
+Arguments invg_inj {T}.
+Prenex Implicits commute invgK.
 
 Section GroupIdentities.
 
@@ -644,9 +644,8 @@ Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))).
 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.
+Arguments commgP {T x y}.
+Arguments conjg_fixP {T x y}.
 
 Section Repr.
 (* Plucking a set representative. *)
@@ -945,9 +944,9 @@ Proof. by apply/setP=> y; rewrite !inE inv_eq //; apply: invgK. Qed.
 
 End BaseSetMulProp.
 
-Arguments set1gP [gT x].
-Arguments mulsgP [gT A B x].
-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 *)
@@ -1303,13 +1302,12 @@ Definition order x := #|cycle x|.
 
 End GroupSetMulProp.
 
-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].
+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.
 
 Arguments commutator _ _%g _%g.
 Arguments joing _ _%g _%g.
@@ -1857,16 +1855,15 @@ Notation "[ 'subg' G ]" := [set: subg_of G]%G : Group_scope.
 Prenex Implicits subg sgval subg_of.
 Bind Scope group_scope with subg_of.
 
-Arguments trivgP [gT G].
-Arguments trivGP [gT G].
-Arguments lcoset_eqP [gT G x y].
-Arguments rcoset_eqP [gT G x y].
+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.
+Arguments comm_group_setP {gT G H}.
+Arguments class_eqP {gT G x y}.
+Arguments repr_classesP {gT G xG}.
 
 Section GroupInter.
 
@@ -2395,11 +2392,11 @@ Qed.
 
 End GeneratedGroup.
 
-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].
+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.
 
@@ -2523,7 +2520,7 @@ Proof.
 suffices ->: (x \in 'N(A)) = (A :^ x == A) by apply: eqP.
 by rewrite eqEcard cardJg leqnn andbT inE.
 Qed.
-Arguments normP [x A].
+Arguments normP {x A}.
 
 Lemma group_set_normaliser A : group_set 'N(A).
 Proof.
@@ -2538,7 +2535,7 @@ Proof.
 apply: (iffP subsetP) => nBA x Ax; last by rewrite inE nBA //.
 by apply/normP; apply: nBA.
 Qed.
-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.
@@ -2986,15 +2983,13 @@ End SubAbelian.
 
 End Normaliser.
 
-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.
+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}.
 
 Arguments normaliser_group _ _%g.
 Arguments centraliser_group _ _%g.
@@ -3090,6 +3085,5 @@ 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.
 
-Arguments mingroupP [gT gP G].
-Arguments maxgroupP [gT gP G].
-Prenex Implicits mingroupP maxgroupP.
+Arguments mingroupP {gT gP G}.
+Arguments maxgroupP {gT gP G}.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 986489b..22c19d4 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -867,11 +867,11 @@ Qed.
 
 End InternalProd.
 
-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].
+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.
 
@@ -1700,5 +1700,5 @@ Qed.
 
 End DirprodIsom.
 
-Arguments mulgmP [gT H1 H2 G].
-Prenex Implicits mulgm mulgmP.
+Arguments mulgmP {gT H1 H2 G}.
+Prenex Implicits mulgm.
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index 3c23921..4b2d863 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -118,9 +118,8 @@ Notation "[ 'morphism' D 'of' f ]" :=
 Notation "[ 'morphism' 'of' f ]" := (clone_morphism (@Morphism _ _ _ f))
    (at level 0, format "[ 'morphism'  'of'  f ]") : form_scope.
 
-Arguments morphimP [aT rT D A y f].
-Arguments morphpreP [aT rT D R x f].
-Prenex Implicits morphimP morphpreP.
+Arguments morphimP {aT rT D A y f}.
+Arguments morphpreP {aT rT D R x f}.
 
 (* Domain, image, preimage, kernel, using phantom types to infer the domain. *)
 
@@ -873,7 +872,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.
 
-Arguments injmP [aT rT D f].
+Arguments injmP {aT rT D f}.
 
 Section IdentityMorphism.
 
@@ -908,8 +907,7 @@ Proof. exact: morphim_idm. Qed.
 
 End IdentityMorphism.
 
-Arguments idm _ _%g _%g.
-Prenex Implicits idm.
+Arguments idm {_} _%g _%g.
 
 Section RestrictedMorphism.
 
@@ -967,10 +965,9 @@ Proof. by move <-; exists f. Qed.
 
 End RestrictedMorphism.
 
-Arguments restrm _ _ _%g _%g _ _%g.
-Prenex Implicits restrm.
-Arguments restrmP [aT rT A D].
-Arguments domP [aT rT A D].
+Arguments restrm {_ _ _%g _%g} _ _%g.
+Arguments restrmP {aT rT A D}.
+Arguments domP {aT rT A D}.
 
 Section TrivMorphism.
 
@@ -1324,17 +1321,17 @@ Proof. exact: restr_isom_to. Qed.
 
 End ReflectProp.
 
-Arguments isom _ _ _%g _%g _.
-Arguments morphic _ _ _%g _.
+Arguments isom {_ _} _%g _%g _.
+Arguments morphic {_ _} _%g _.
 Arguments misom _ _ _%g _%g _.
-Arguments isog _ _ _%g _%g.
+Arguments isog {_ _} _%g _%g.
 
-Arguments morphicP [aT rT A f].
-Arguments misomP [aT rT A B f].
+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.
+Arguments isomP {aT rT G H f}.
+Arguments isogP {aT rT G H}.
+Prenex Implicits morphm.
 Notation "x \isog y":= (isog x y).
 
 Section Isomorphisms.
@@ -1482,7 +1479,7 @@ Arguments homg _ _ _%g _%g.
 Notation "G \homg H" := (homg G H)
   (at level 70, no associativity) : group_scope.
 
-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 3edcfed..01ef08e 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -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].
-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.
-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 03c55b3..322fc4e 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.v
@@ -198,10 +198,9 @@ Lemma quotientE : quotient = coset @* Q. Proof. by []. Qed.
 
 End Cosets.
 
-Arguments coset_of _ _%g.
-Arguments coset _ _%g _%g.
+Arguments coset_of {_} _%g.
+Arguments coset {_} _%g _%g.
 Arguments quotient _ _%g _%g.
-Prenex Implicits coset_of coset.
 
 Bind Scope group_scope with coset_of.