Change Implicit Arguments to Arguments in field

6 files changed, 39 insertions, 39 deletions

diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 891bce5..3696316 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -260,7 +260,7 @@ Qed.
 Prenex Implicits alg_integral.
 
 Import DefaultKeying GRing.DefaultPred.
-Implicit Arguments map_poly_inj [[F] [R] x1 x2].
+Arguments map_poly_inj {F R} f [x1 x2].
 
 Theorem Fundamental_Theorem_of_Algebraics :
   {L : closedFieldType &
diff --git a/mathcomp/field/countalg.v b/mathcomp/field/countalg.v
index 95d28cb..a6d11b3 100644
--- a/mathcomp/field/countalg.v
+++ b/mathcomp/field/countalg.v
@@ -59,7 +59,7 @@ Definition gen_pack T :=
 
 End Generic.
 
-Implicit Arguments gen_pack [type base_type class_of base_of base_sort].
+Arguments gen_pack [type base_type class_of base_of base_sort].
 Local Notation cnt_ c := (@Countable.Class _ c c).
 Local Notation do_pack pack T := (pack T _ _ id _ _ _ id).
 Import GRing.Theory.
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index 995dbee..e0ae1b1 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -641,12 +641,12 @@ Notation "[ 'aspace' 'of' U ]" := (@clone_aspace _ _ U _ _ id)
 Notation "[ 'aspace' 'of' U 'for' A ]" := (@clone_aspace _ _ U A _ idfun)
   (at level 0, format "[ 'aspace'  'of'  U  'for'  A ]") : form_scope.
 
-Implicit Arguments prodvP [K aT U V W].
-Implicit Arguments cent1vP [K aT u v].
-Implicit Arguments centvP [K aT u V].
-Implicit Arguments centvsP [K aT U V].
-Implicit Arguments has_algidP [K aT U].
-Implicit Arguments polyOver1P [K aT p].
+Arguments prodvP [K aT U V W].
+Arguments cent1vP [K aT u v].
+Arguments centvP [K aT u V].
+Arguments centvsP [K aT U V].
+Arguments has_algidP [K aT U].
+Arguments polyOver1P [K aT p].
 
 Section AspaceTheory.
 
@@ -856,8 +856,8 @@ Notation "'C [ u ]" := (centraliser1_aspace u) : aspace_scope.
 Notation "'C ( V )" := (centraliser_aspace V) : aspace_scope.
 Notation "'Z ( A )" := (center_aspace A) : aspace_scope.
 
-Implicit Arguments adim1P [K aT A].
-Implicit Arguments memv_cosetP [K aT U v w].
+Arguments adim1P [K aT A].
+Arguments memv_cosetP [K aT U v w].
 
 Section Closure.
 
@@ -1117,9 +1117,9 @@ Canonical linfun_ahom f := AHom (linfun_is_ahom f).
 
 End Class_Def.
 
-Implicit Arguments ahom_in [aT rT].
-Implicit Arguments ahom_inP [aT rT f U].
-Implicit Arguments ahomP [aT rT f].
+Arguments ahom_in [aT rT].
+Arguments ahom_inP [aT rT f U].
+Arguments ahomP [aT rT f].
 
 Section LRMorphism.
 
@@ -1196,7 +1196,7 @@ Canonical fixedSpace_aspace aT (f : ahom aT aT) := [aspace of fixedSpace f].
 
 End AHom.
 
-Implicit Arguments ahom_in [K aT rT].
+Arguments ahom_in [K aT rT].
 
 Notation "''AHom' ( aT , rT )" := (ahom aT rT) : type_scope.
 Notation "''AEnd' ( aT )" := (ahom aT aT) : type_scope.
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 8d2af81..2a905e9 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -696,7 +696,7 @@ move=> sKE; apply: minPoly_dvdp; last exact: root_minPoly.
 by apply: (polyOverSv sKE); rewrite minPolyOver.
 Qed.
 
-Implicit Arguments Fadjoin_polyP [K x v].
+Arguments Fadjoin_polyP [K x v].
 Lemma Fadjoin1_polyP x v :
   reflect (exists p, v = (map_poly (in_alg L) p).[x]) (v \in <<1; x>>%VS).
 Proof.
@@ -737,13 +737,13 @@ Notation "'C_ ( E ) ( V )" := (capv_aspace E 'C(V))
 Notation "E * F" := (prodv_aspace E F) : aspace_scope.
 Notation "f @: E" := (aimg_aspace f E) : aspace_scope.
 
-Implicit Arguments Fadjoin_idP [F0 L K x].
-Implicit Arguments FadjoinP [F0 L K x E].
-Implicit Arguments Fadjoin_seqP [F0 L K rs E].
-Implicit Arguments polyOver_subvs [F0 L K p].
-Implicit Arguments Fadjoin_polyP [F0 L K x v].
-Implicit Arguments Fadjoin1_polyP [F0 L x v].
-Implicit Arguments minPoly_XsubC [F0 L K x].
+Arguments Fadjoin_idP [F0 L K x].
+Arguments FadjoinP [F0 L K x E].
+Arguments Fadjoin_seqP [F0 L K rs E].
+Arguments polyOver_subvs [F0 L K p].
+Arguments Fadjoin_polyP [F0 L K x v].
+Arguments Fadjoin1_polyP [F0 L x v].
+Arguments minPoly_XsubC [F0 L K x].
 
 Section MapMinPoly.
 
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index eaf5709..7e2fa17 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -329,9 +329,9 @@ End kHom.
 
 Notation "f ^-1" := (inv_ahom f) : lrfun_scope.
 
-Implicit Arguments kHomP [F L K V f].
-Implicit Arguments kAHomP [F L U V f].
-Implicit Arguments kHom_lrmorphism [F L f].
+Arguments kHomP [F L K V f].
+Arguments kAHomP [F L U V f].
+Arguments kHom_lrmorphism [F L f].
 
 Module SplittingField.
 
@@ -1205,7 +1205,7 @@ have [x galEx Df] := kHom_to_gal sK_Ka_E nKE homKa_f; exists x => //.
 by rewrite -Df ?memv_adjoin // (kHomExtend_val (kHom1 K K)) ?lfun1_poly.
 Qed.
 
-Implicit Arguments normalFieldP [K E].
+Arguments normalFieldP [K E].
 
 Lemma normalField_factors K E :
    (K <= E)%VS ->
@@ -1637,7 +1637,7 @@ End GaloisTheory.
 Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
 Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.
 
-Implicit Arguments fixedFieldP [F L E A a].
-Implicit Arguments normalFieldP [F L K E].
-Implicit Arguments splitting_galoisField [F L K E].
-Implicit Arguments galois_fixedField [F L K E].
+Arguments fixedFieldP [F L E A a].
+Arguments normalFieldP [F L K E].
+Arguments splitting_galoisField [F L K E].
+Arguments galois_fixedField [F L K E].
diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v
index c3f3ebb..c5a1118 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -170,7 +170,7 @@ Qed.
 
 End SeparablePoly.
 
-Implicit Arguments separable_polyP [R p].
+Arguments separable_polyP [R p].
 
 Lemma separable_map (F : fieldType) (R : idomainType)
                     (f : {rmorphism F -> R}) (p : {poly F}) :
@@ -544,7 +544,7 @@ Qed.
 
 End SeparableElement.
 
-Implicit Arguments separable_elementP [K x].
+Arguments separable_elementP [K x].
 
 Lemma separable_elementS K E x :
   (K <= E)%VS -> separable_element K x -> separable_element E x.
@@ -992,10 +992,10 @@ Qed.
 
 End Separable.
 
-Implicit Arguments separable_elementP [F L K x].
-Implicit Arguments separablePn [F L K x].
-Implicit Arguments Derivation_separableP [F L K x].
-Implicit Arguments adjoin_separableP [F L K x].
-Implicit Arguments purely_inseparable_elementP [F L K x].
-Implicit Arguments separableP [F L K E].
-Implicit Arguments purely_inseparableP [F L K E].
+Arguments separable_elementP [F L K x].
+Arguments separablePn [F L K x].
+Arguments Derivation_separableP [F L K x].
+Arguments adjoin_separableP [F L K x].
+Arguments purely_inseparable_elementP [F L K x].
+Arguments separableP [F L K E].
+Arguments purely_inseparableP [F L K E].