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

Merge Arguments and Prenex Implicits

4 files changed, 35 insertions, 35 deletions

diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index ada61bc..0410e55 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.
 
-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].
+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.
 
-Arguments adim1P [K aT A].
-Arguments memv_cosetP [K aT U v w].
+Arguments adim1P {K aT A}.
+Arguments memv_cosetP {K aT U v w}.
 
 Section Closure.
 
@@ -1118,8 +1118,8 @@ Canonical linfun_ahom f := AHom (linfun_is_ahom f).
 End Class_Def.
 
 Arguments ahom_in [aT rT].
-Arguments ahom_inP [aT rT f U].
-Arguments ahomP [aT rT f].
+Arguments ahom_inP {aT rT f U}.
+Arguments ahomP {aT rT f}.
 
 Section LRMorphism.
 
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 2a905e9..881b888 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.
 
-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.
 
-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].
+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 7e2fa17..2ed40e1 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.
 
-Arguments kHomP [F L K V f].
-Arguments kAHomP [F L U V f].
-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.
 
-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.
 
-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].
+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 8185314..528b314 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -170,7 +170,7 @@ Qed.
 
 End SeparablePoly.
 
-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.
 
-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.
 
-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].
+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}.