From 40d53fc61a7907c7f08bf37b9ab045ef4a5a1fe9 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 21 Feb 2018 23:48:01 -0800
Subject: Change Implicit Arguments to Arguments in field

---
 mathcomp/field/fieldext.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'mathcomp/field/fieldext.v')

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.
 
-- 
cgit v1.2.3