Merge pull request #179 from jashug/deprecate-implicit-arguments

Remove Implicit Arguments command in favor of Arguments

1 files changed, 8 insertions, 8 deletions

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.