Change Implicit Arguments to Arguments in ssreflect

14 files changed, 241 insertions, 241 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 941b488..64e8927 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -678,7 +678,7 @@ Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F :
   -> K' (\big[op/idx]_(i <- r | P i) F i).
 Proof. by case. Qed.
 
-Implicit Arguments big_load [R K' I].
+Arguments big_load [R] K [K'] idx op [I].
 
 Section Elim3.
 
@@ -708,8 +708,8 @@ Proof. by apply: big_rec3 => i x1 x2 x3 /K_F; apply: Kop. Qed.
 
 End Elim3.
 
-Implicit Arguments big_rec3 [R1 R2 R3 id1 op1 id2 op2 id3 op3 I r P F1 F2 F3].
-Implicit Arguments big_ind3 [R1 R2 R3 id1 op1 id2 op2 id3 op3 I r P F1 F2 F3].
+Arguments big_rec3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ [I r P F1 F2 F3].
+Arguments big_ind3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ _ [I r P F1 F2 F3].
 
 Section Elim2.
 
@@ -738,9 +738,9 @@ Proof. by rewrite unlock; elim: r => //= i r <-; rewrite -f_op -fun_if. Qed.
 
 End Elim2.
 
-Implicit Arguments big_rec2 [R1 R2 id1 op1 id2 op2 I r P F1 F2].
-Implicit Arguments big_ind2 [R1 R2 id1 op1 id2 op2 I r P F1 F2].
-Implicit Arguments big_morph [R1 R2 id1 op1 id2 op2 I].
+Arguments big_rec2 [R1 R2] K [id1 op1 id2 op2] _ [I r P F1 F2].
+Arguments big_ind2 [R1 R2] K [id1 op1 id2 op2] _ _ [I r P F1 F2].
+Arguments big_morph [R1 R2] f [id1 op1 id2 op2] _ _ [I].
 
 Section Elim1.
 
@@ -773,10 +773,10 @@ Proof. exact: big_morph. Qed.
 
 End Elim1.
 
-Implicit Arguments big_rec [R idx op I r P F].
-Implicit Arguments big_ind [R idx op I r P F].
-Implicit Arguments eq_big_op [R idx op I].
-Implicit Arguments big_endo [R idx op I].
+Arguments big_rec [R] K [idx op] _ [I r P F].
+Arguments big_ind [R] K [idx op] _ _ [I r P F].
+Arguments eq_big_op [R] K [idx op] op' _ _ _ [I].
+Arguments big_endo [R] f [idx op] _ _ [I].
 
 Section Extensionality.
 
@@ -1306,7 +1306,7 @@ Proof.
 rewrite !(big_mkcond _ _ _ F) -big_split.
 by apply: eq_bigr => i; case: (a i); rewrite !simpm.
 Qed.
-Implicit Arguments bigID [I r].
+Arguments bigID [I r].
 
 Lemma bigU (I : finType) (A B : pred I) F :
     [disjoint A & B] ->
@@ -1325,7 +1325,7 @@ Proof.
 move=> Pj; rewrite (bigID (pred1 j)); congr (_ * _).
 by apply: big_pred1 => i; rewrite /= andbC; case: eqP => // ->.
 Qed.
-Implicit Arguments bigD1 [I P F].
+Arguments bigD1 [I] j [P F].
 
 Lemma bigD1_seq (I : eqType) (r : seq I) j F : 
     j \in r -> uniq r ->
@@ -1338,7 +1338,7 @@ Proof.
 move=> Aj; rewrite (cardD1 j) [j \in A]Aj; congr (_ + _).
 by apply: eq_card => i; rewrite inE /= andbC.
 Qed.
-Implicit Arguments cardD1x [I A].
+Arguments cardD1x [I A].
 
 Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) F :
     (forall i, P i -> Q (p i)) ->
@@ -1356,7 +1356,7 @@ rewrite (bigID (fun i => p i == j)); congr (_ * _); apply: eq_bigl => i.
 by rewrite andbA.
 Qed.
 
-Implicit Arguments partition_big [I J P F].
+Arguments partition_big [I J P] p Q [F].
 
 Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F :
    (forall i, P i -> h (h' i) = i) ->
@@ -1372,7 +1372,7 @@ rewrite {}IH => [|j]; [apply: eq_bigl => j | by case/andP; auto].
 rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK; congr (_ && ~~ _).
 by apply/eqP/eqP=> [<-|->] //; rewrite h'K.
 Qed.
-Implicit Arguments reindex_onto [I J P F].
+Arguments reindex_onto [I J] h h' [P F].
 
 Lemma reindex (I J : finType) (h : J -> I) (P : pred I) F :
     {on [pred i | P i], bijective h} ->
@@ -1381,12 +1381,12 @@ Proof.
 case=> h' hK h'K; rewrite (reindex_onto h h' h'K).
 by apply: eq_bigl => j; rewrite !inE; case Pi: (P _); rewrite //= hK ?eqxx.
 Qed.
-Implicit Arguments reindex [I J P F].
+Arguments reindex [I J] h [P F].
 
 Lemma reindex_inj (I : finType) (h : I -> I) (P : pred I) F :
   injective h -> \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j)) F (h j).
 Proof. by move=> injh; apply: reindex (onW_bij _ (injF_bij injh)). Qed.
-Implicit Arguments reindex_inj [I h P F].
+Arguments reindex_inj [I h P F].
 
 Lemma big_nat_rev m n P F :
   \big[*%M/1]_(m <= i < n | P i) F i
@@ -1430,7 +1430,7 @@ rewrite !pair_big_dep (reindex_onto (p _ _) (p _ _)) => [|[]] //=.
 apply: eq_big => [] [j i] //=; symmetry; rewrite eqxx andbT andb_idl //.
 by case/andP; apply: PQxQ.
 Qed.
-Implicit Arguments exchange_big_dep [I J rI rJ P Q F].
+Arguments exchange_big_dep [I J rI rJ P Q] xQ [F].
 
 Lemma exchange_big I J rI rJ (P : pred I) (Q : pred J) F :
   \big[*%M/1]_(i <- rI | P i) \big[*%M/1]_(j <- rJ | Q j) F i j =
@@ -1453,7 +1453,7 @@ rewrite big_seq_cond /= (exchange_big_dep xQ) => [|i j]; last first.
 rewrite 2!(big_seq_cond _ _ _ xQ); apply: eq_bigr => j /andP[-> _] /=.
 by rewrite [rhs in _ = rhs]big_seq_cond; apply: eq_bigl => i; rewrite -andbA.
 Qed.
-Implicit Arguments exchange_big_dep_nat [m1 n1 m2 n2 P Q F].
+Arguments exchange_big_dep_nat [m1 n1 m2 n2 P Q] xQ [F].
 
 Lemma exchange_big_nat m1 n1 m2 n2 (P Q : pred nat) F :
   \big[*%M/1]_(m1 <= i < n1 | P i) \big[*%M/1]_(m2 <= j < n2 | Q j) F i j =
@@ -1467,58 +1467,58 @@ End Abelian.
 
 End MonoidProperties.
 
-Implicit Arguments big_filter [R op idx I].
-Implicit Arguments big_filter_cond [R op idx I].
-Implicit Arguments congr_big [R op idx I r1 P1 F1].
-Implicit Arguments eq_big [R op idx I r P1 F1].
-Implicit Arguments eq_bigl [R op idx  I r P1].
-Implicit Arguments eq_bigr [R op idx I r  P F1].
-Implicit Arguments eq_big_idx [R op idx idx' I P F].
-Implicit Arguments big_seq_cond [R op idx I r].
-Implicit Arguments eq_big_seq [R op idx I r F1].
-Implicit Arguments congr_big_nat [R op idx m1 n1 P1 F1].
-Implicit Arguments big_map [R op idx I J r].
-Implicit Arguments big_nth [R op idx I r].
-Implicit Arguments big_catl [R op idx I r1 r2 P F].
-Implicit Arguments big_catr [R op idx I r1 r2  P F].
-Implicit Arguments big_geq [R op idx m n P F].
-Implicit Arguments big_ltn_cond [R op idx m n P F].
-Implicit Arguments big_ltn [R op idx m n F].
-Implicit Arguments big_addn [R op idx].
-Implicit Arguments big_mkord [R op idx n].
-Implicit Arguments big_nat_widen [R op idx] .
-Implicit Arguments big_ord_widen_cond [R op idx n1].
-Implicit Arguments big_ord_widen [R op idx n1].
-Implicit Arguments big_ord_widen_leq [R op idx n1].
-Implicit Arguments big_ord_narrow_cond [R op idx n1 n2 P F].
-Implicit Arguments big_ord_narrow_cond_leq [R op idx n1 n2 P F].
-Implicit Arguments big_ord_narrow [R op idx n1 n2 F].
-Implicit Arguments big_ord_narrow_leq [R op idx n1 n2 F].
-Implicit Arguments big_mkcond [R op idx I r].
-Implicit Arguments big1_eq [R op idx I].
-Implicit Arguments big1_seq [R op idx I].
-Implicit Arguments big1 [R op idx I].
-Implicit Arguments big_pred1 [R op idx I P F].
-Implicit Arguments eq_big_perm [R op idx I r1 P F].
-Implicit Arguments big_uniq [R op idx I F].
-Implicit Arguments big_rem [R op idx I r P F].
-Implicit Arguments bigID [R op idx I r].
-Implicit Arguments bigU [R op idx I].
-Implicit Arguments bigD1 [R op idx I P F].
-Implicit Arguments bigD1_seq [R op idx I r F].
-Implicit Arguments partition_big [R op idx I J P F].
-Implicit Arguments reindex_onto [R op idx I J P F].
-Implicit Arguments reindex [R op idx I J P F].
-Implicit Arguments reindex_inj [R op idx I h P F].
-Implicit Arguments pair_big_dep [R op idx I J].
-Implicit Arguments pair_big [R op idx I J].
-Implicit Arguments big_allpairs [R op idx I1 I2 r1 r2 F].
-Implicit Arguments exchange_big_dep [R op idx I J rI rJ P Q F].
-Implicit Arguments exchange_big_dep_nat [R op idx m1 n1 m2 n2 P Q F].
-Implicit Arguments big_ord_recl [R op idx].
-Implicit Arguments big_ord_recr [R op idx].
-Implicit Arguments big_nat_recl [R op idx].
-Implicit Arguments big_nat_recr [R op idx].
+Arguments big_filter [R idx op I].
+Arguments big_filter_cond [R idx op I].
+Arguments congr_big [R idx op I r1] r2 [P1] P2 [F1] F2.
+Arguments eq_big [R idx op I r P1] P2 [F1] F2.
+Arguments eq_bigl [R idx op I r P1] P2.
+Arguments eq_bigr [R idx op I r P F1] F2.
+Arguments eq_big_idx [R idx op idx' I] i0 [P F].
+Arguments big_seq_cond [R idx op I r].
+Arguments eq_big_seq [R idx op I r F1] F2.
+Arguments congr_big_nat [R idx op m1 n1] m2 n2 [P1] P2 [F1] F2.
+Arguments big_map [R idx op I J] h [r].
+Arguments big_nth [R idx op I] x0 [r].
+Arguments big_catl [R idx op I r1 r2 P F].
+Arguments big_catr [R idx op I r1 r2 P F].
+Arguments big_geq [R idx op m n P F].
+Arguments big_ltn_cond [R idx op m n P F].
+Arguments big_ltn [R idx op m n F].
+Arguments big_addn [R idx op].
+Arguments big_mkord [R idx op n].
+Arguments big_nat_widen [R idx op] .
+Arguments big_ord_widen_cond [R idx op n1].
+Arguments big_ord_widen [R idx op n1].
+Arguments big_ord_widen_leq [R idx op n1].
+Arguments big_ord_narrow_cond [R idx op n1 n2 P F].
+Arguments big_ord_narrow_cond_leq [R idx op n1 n2 P F].
+Arguments big_ord_narrow [R idx op n1 n2 F].
+Arguments big_ord_narrow_leq [R idx op n1 n2 F].
+Arguments big_mkcond [R idx op I r].
+Arguments big1_eq [R idx op I].
+Arguments big1_seq [R idx op I].
+Arguments big1 [R idx op I].
+Arguments big_pred1 [R idx op I] i [P F].
+Arguments eq_big_perm [R idx op I r1] r2 [P F].
+Arguments big_uniq [R idx op I] r [F].
+Arguments big_rem [R idx op I r] x [P F].
+Arguments bigID [R idx op I r].
+Arguments bigU [R idx op I].
+Arguments bigD1 [R idx op I] j [P F].
+Arguments bigD1_seq [R idx op I r] j [F].
+Arguments partition_big [R idx op I J P] p Q [F].
+Arguments reindex_onto [R idx op I J] h h' [P F].
+Arguments reindex [R idx op I J] h [P F].
+Arguments reindex_inj [R idx op I h P F].
+Arguments pair_big_dep [R idx op I J].
+Arguments pair_big [R idx op I J].
+Arguments big_allpairs [R idx op I1 I2 r1 r2 F].
+Arguments exchange_big_dep [R idx op I J rI rJ P Q] xQ [F].
+Arguments exchange_big_dep_nat [R idx op m1 n1 m2 n2 P Q] xQ [F].
+Arguments big_ord_recl [R idx op].
+Arguments big_ord_recr [R idx op].
+Arguments big_nat_recl [R idx op].
+Arguments big_nat_recr [R idx op].
 
 Section Distributivity.
 
@@ -1614,13 +1614,13 @@ Proof. by rewrite bigA_distr_big; apply: eq_bigl => ?; apply/familyP. Qed.
 
 End Distributivity.
 
-Implicit Arguments big_distrl [R zero times plus I r].
-Implicit Arguments big_distrr [R zero times plus I r].
-Implicit Arguments big_distr_big_dep [R zero one times plus I J].
-Implicit Arguments big_distr_big [R zero one times plus I J].
-Implicit Arguments bigA_distr_big_dep [R zero one times plus I J].
-Implicit Arguments bigA_distr_big [R zero one times plus I J].
-Implicit Arguments bigA_distr_bigA [R zero one times plus I J].
+Arguments big_distrl [R zero times plus I r].
+Arguments big_distrr [R zero times plus I r].
+Arguments big_distr_big_dep [R zero one times plus I J].
+Arguments big_distr_big [R zero one times plus I J].
+Arguments bigA_distr_big_dep [R zero one times plus I J].
+Arguments bigA_distr_big [R zero one times plus I J].
+Arguments bigA_distr_bigA [R zero one times plus I J].
 
 Section BigBool.
 
@@ -1715,11 +1715,11 @@ Proof. by move=> Fpos; apply: prodn_cond_gt0. Qed.
 Lemma leq_bigmax_cond (I : finType) (P : pred I) F i0 :
   P i0 -> F i0 <= \max_(i | P i) F i.
 Proof. by move=> Pi0; rewrite (bigD1 i0) ?leq_maxl. Qed.
-Implicit Arguments leq_bigmax_cond [I P F].
+Arguments leq_bigmax_cond [I P F].
 
 Lemma leq_bigmax (I : finType) F (i0 : I) : F i0 <= \max_i F i.
 Proof. exact: leq_bigmax_cond. Qed.
-Implicit Arguments leq_bigmax [I F].
+Arguments leq_bigmax [I F].
 
 Lemma bigmax_leqP (I : finType) (P : pred I) m F :
   reflect (forall i, P i -> F i <= m) (\max_(i | P i) F i <= m).
@@ -1732,7 +1732,7 @@ Qed.
 Lemma bigmax_sup (I : finType) i0 (P : pred I) m F :
   P i0 -> m <= F i0 -> m <= \max_(i | P i) F i.
 Proof. by move=> Pi0 le_m_Fi0; apply: leq_trans (leq_bigmax_cond i0 Pi0). Qed.
-Implicit Arguments bigmax_sup [I P m F].
+Arguments bigmax_sup [I] i0 [P m F].
 
 Lemma bigmax_eq_arg (I : finType) i0 (P : pred I) F :
   P i0 -> \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i].
@@ -1740,7 +1740,7 @@ Proof.
 move=> Pi0; case: arg_maxP => //= i Pi maxFi.
 by apply/eqP; rewrite eqn_leq leq_bigmax_cond // andbT; apply/bigmax_leqP.
 Qed.
-Implicit Arguments bigmax_eq_arg [I P F].
+Arguments bigmax_eq_arg [I] i0 [P F].
 
 Lemma eq_bigmax_cond (I : finType) (A : pred I) F :
   #|A| > 0 -> {i0 | i0 \in A & \max_(i in A) F i = F i0}.
@@ -1769,7 +1769,7 @@ Lemma biglcmn_sup (I : finType) i0 (P : pred I) F m :
 Proof.
 by move=> Pi0 m_Fi0; rewrite (dvdn_trans m_Fi0) // (bigD1 i0) ?dvdn_lcml.
 Qed.
-Implicit Arguments biglcmn_sup [I P F m].
+Arguments biglcmn_sup [I] i0 [P F m].
 
 Lemma dvdn_biggcdP (I : finType) (P : pred I) F m :
   reflect (forall i, P i -> m %| F i) (m %| \big[gcdn/0]_(i | P i) F i).
@@ -1782,6 +1782,6 @@ Qed.
 Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m :
   P i0 -> F i0 %| m -> \big[gcdn/0]_(i | P i) F i %| m.
 Proof. by move=> Pi0; apply: dvdn_trans; rewrite (bigD1 i0) ?dvdn_gcdl. Qed.
-Implicit Arguments biggcdn_inf [I P F m].
+Arguments biggcdn_inf [I] i0 [P F m].
 
 Unset Implicit Arguments.
diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index a696bbd..b5c2391 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -193,7 +193,7 @@ Qed.
 End Def.
 
 End GenTree.
-Implicit Arguments GenTree.codeK [].
+Arguments GenTree.codeK : clear implicits.
 
 Definition tree_eqMixin (T : eqType) := PcanEqMixin (GenTree.codeK T).
 Canonical tree_eqType (T : eqType) := EqType (GenTree.tree T) (tree_eqMixin T).
@@ -558,7 +558,7 @@ Export Countable.Exports.
 
 Definition unpickle T := Countable.unpickle (Countable.class T).
 Definition pickle T := Countable.pickle (Countable.class T).
-Implicit Arguments unpickle [T].
+Arguments unpickle [T].
 Prenex Implicits pickle unpickle.
 
 Section CountableTheory.
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 4172430..59c19ce 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -130,11 +130,11 @@ rewrite {2}/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd.
 rewrite mulnDr mulnCA divnMDl; last by rewrite muln_gt0 p_gt0.
 by rewrite addnC divn_small // ltn_pmul2l.
 Qed.
-Implicit Arguments divnMl [p m d].
+Arguments divnMl [p m d].
 
 Lemma divnMr p m d : p > 0 -> m * p %/ (d * p) = m %/ d.
 Proof. by move=> p_gt0; rewrite -!(mulnC p) divnMl. Qed.
-Implicit Arguments divnMr [p m d].
+Arguments divnMr [p m d].
 
 Lemma ltn_mod m d : (m %% d < d) = (0 < d).
 Proof. by case: d => // d; rewrite modn_def; case: edivnP. Qed.
@@ -302,7 +302,7 @@ Proof.
 apply: (iffP eqP) => [md0 | [k ->]]; last by rewrite modnMl.
 by exists (m %/ d); rewrite {1}(divn_eq m d) md0 addn0.
 Qed.
-Implicit Arguments dvdnP [d m].
+Arguments dvdnP [d m].
 Prenex Implicits dvdnP.
 
 Lemma dvdn0 d : d %| 0.
@@ -401,11 +401,11 @@ Qed.
 
 Lemma dvdn_pmul2l p d m : 0 < p -> (p * d %| p * m) = (d %| m).
 Proof. by case: p => // p _; rewrite /dvdn -muln_modr // muln_eq0. Qed.
-Implicit Arguments dvdn_pmul2l [p m d].
+Arguments dvdn_pmul2l [p d m].
 
 Lemma dvdn_pmul2r p d m : 0 < p -> (d * p %| m * p) = (d %| m).
 Proof. by move=> p_gt0; rewrite -!(mulnC p) dvdn_pmul2l. Qed.
-Implicit Arguments dvdn_pmul2r [p m d].
+Arguments dvdn_pmul2r [p d m].
 
 Lemma dvdn_divLR p d m : 0 < p -> p %| d -> (d %/ p %| m) = (d %| m * p).
 Proof. by move=> /(@dvdn_pmul2r p _ m) <- /divnK->. Qed.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 3e8230e..9772b84 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -147,7 +147,7 @@ Proof. by []. Qed.
 
 Lemma eqP T : Equality.axiom (@eq_op T).
 Proof. by case: T => ? []. Qed.
-Implicit Arguments eqP [T x y].
+Arguments eqP [T x y].
 
 Delimit Scope eq_scope with EQ.
 Open Scope eq_scope.
@@ -230,8 +230,8 @@ Proof. by rewrite eq_sym; apply: ifN. Qed.
 
 End Contrapositives.
 
-Implicit Arguments memPn [T1 A x].
-Implicit Arguments memPnC [T1 A x].
+Arguments memPn [T1 A x].
+Arguments memPnC [T1 A x].
 
 Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2.
 Proof.
@@ -339,9 +339,9 @@ Proof. by case: eqP; [left | right]. Qed.
 
 End EqPred.
 
-Implicit Arguments predU1P [T x y b].
-Implicit Arguments pred2P [T T2 x y z u].
-Implicit Arguments predD1P [T x y b].
+Arguments predU1P [T x y b].
+Arguments pred2P [T T2 x y z u].
+Arguments predD1P [T x y b].
 Prenex Implicits pred1 pred2 pred3 pred4 predU1 predC1 predD1 predU1P.
 
 Notation "[ 'predU1' x & A ]" := (predU1 x [mem A])
@@ -491,7 +491,7 @@ Structure subType : Type := SubType {
   _ : forall x Px, val (@Sub x Px) = x
 }.
 
-Implicit Arguments Sub [s].
+Arguments Sub [s].
 Lemma vrefl : forall x, P x -> x = x. Proof. by []. Qed.
 Definition vrefl_rect := vrefl.
 
@@ -572,14 +572,14 @@ Qed.
 
 End SubType.
 
-Implicit Arguments SubType [T P].
-Implicit Arguments Sub [T P s].
-Implicit Arguments vrefl [T P].
-Implicit Arguments vrefl_rect [T P].
-Implicit Arguments clone_subType [T P sT c Urec cK].
-Implicit Arguments insub [T P sT].
-Implicit Arguments insubT [T sT x].
-Implicit Arguments val_inj [T P sT].
+Arguments SubType [T P].
+Arguments Sub [T P s].
+Arguments vrefl [T P].
+Arguments vrefl_rect [T P].
+Arguments clone_subType [T P] U v [sT] _ [c Urec cK].
+Arguments insub [T P sT].
+Arguments insubT [T] P [sT x].
+Arguments val_inj [T P sT].
 Prenex Implicits val Sub vrefl vrefl_rect insub insubd val_inj.
 
 Local Notation inlined_sub_rect :=
@@ -610,7 +610,7 @@ Notation "[ 'subType' 'of' U ]" := (clone_subType U _ id id)
 Definition NewType T U v c Urec :=
   let Urec' P IH := Urec P (fun x : T => IH x isT : P _) in
   SubType U v (fun x _ => c x) Urec'.
-Implicit Arguments NewType [T U].
+Arguments NewType [T U].
 
 Notation "[ 'newType' 'for' v ]" := (NewType v _ inlined_new_rect vrefl_rect)
  (at level 0, only parsing) : form_scope.
@@ -622,7 +622,7 @@ Notation "[ 'newType' 'for' v 'by' rec ]" := (NewType v _ rec vrefl)
  (at level 0, format "[ 'newType'  'for'  v  'by'  rec ]") : form_scope.
 
 Definition innew T nT x := @Sub T predT nT x (erefl true).
-Implicit Arguments innew [T nT].
+Arguments innew [T nT].
 Prenex Implicits innew.
 
 Lemma innew_val T nT : cancel val (@innew T nT).
@@ -713,7 +713,7 @@ Proof. by []. Qed.
 
 End SubEqType.
 
-Implicit Arguments val_eqP [T P sT x y].
+Arguments val_eqP [T P sT x y].
 Prenex Implicits val_eqP.
 
 Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T)
@@ -757,7 +757,7 @@ Proof. by case/andP. Qed.
 
 End ProdEqType.
 
-Implicit Arguments pair_eqP [T1 T2].
+Arguments pair_eqP [T1 T2].
 
 Prenex Implicits pair_eqP.
 
@@ -787,7 +787,7 @@ End OptionEqType.
 Definition tag := projS1.
 Definition tagged I T_ :  forall u, T_(tag u) := @projS2 I [eta T_].
 Definition Tagged I i T_ x := @existS I [eta T_] i x.
-Implicit Arguments Tagged [I i].
+Arguments Tagged [I i].
 Prenex Implicits tag tagged Tagged.
 
 Section TaggedAs.
@@ -834,7 +834,7 @@ Proof. by rewrite -tag_eqE /tag_eq eqxx tagged_asE. Qed.
 
 End TagEqType.
 
-Implicit Arguments tag_eqP [I T_ x y].
+Arguments tag_eqP [I T_ x y].
 Prenex Implicits tag_eqP.
 
 Section SumEqType.
@@ -858,5 +858,5 @@ Lemma sum_eqE : sum_eq = eq_op. Proof. by []. Qed.
 
 End SumEqType.
 
-Implicit Arguments sum_eqP [T1 T2 x y].
+Arguments sum_eqP [T1 T2 x y].
 Prenex Implicits sum_eqP.
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 43ba42a..8b85320 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -147,8 +147,8 @@ End PlainTheory.
 Notation family F := (family_mem (fun_of_simpl (fmem F))).
 Notation ffun_on R := (ffun_on_mem _ (mem R)).
 
-Implicit Arguments familyP [aT rT pT F f].
-Implicit Arguments ffun_onP [aT rT R f].
+Arguments familyP [aT rT pT F f].
+Arguments ffun_onP [aT rT R f].
 
 (*****************************************************************************)
 
@@ -213,7 +213,7 @@ Qed.
 
 End EqTheory.
 
-Implicit Arguments supportP [aT rT y D g].
+Arguments supportP [aT rT y D g].
 Notation pfamily y D F := (pfamily_mem y (mem D) (fun_of_simpl (fmem F))).
 Notation pffun_on y D R := (pffun_on_mem y (mem D) (mem R)).
 
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index dfba3c7..baf5efe 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -224,9 +224,9 @@ Notation closure e a := (closure_mem e (mem a)).
 
 Prenex Implicits connect root roots.
 
-Implicit Arguments dfsP [T g x y].
-Implicit Arguments connectP [T e x y].
-Implicit Arguments rootP [T e x y].
+Arguments dfsP [T g x y].
+Arguments connectP [T e x y].
+Arguments rootP [T e] _ [x y].
 
 Notation fconnect f := (connect (coerced_frel f)).
 Notation froot f := (root (coerced_frel f)).
@@ -770,7 +770,7 @@ Notation "@ 'fun_adjunction' T T' h f f' a" :=
   (@rel_adjunction T T' h (frel f) (frel f') a)
   (at level 10, T, T', h, f, f', a at level 8, only parsing) : type_scope.
 
-Implicit Arguments intro_adjunction [T T' h e e' a].
-Implicit Arguments adjunction_n_comp [T T' e e' a].
+Arguments intro_adjunction [T T' h e e'] _ [a].
+Arguments adjunction_n_comp [T T'] h [e e'] _ _ [a].
 
 Unset Implicit Arguments.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index dc964b5..3f99e9f 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -243,7 +243,7 @@ End BasicSetTheory.
 
 Definition inE := (in_set, inE).
 
-Implicit Arguments set0 [T].
+Arguments set0 [T].
 Prenex Implicits set0.
 Hint Resolve in_setT.
 
@@ -827,7 +827,7 @@ Proof.
 apply: (iffP subsetP) => [sAB | <- x /setIP[] //].
 by apply/setP=> x; rewrite inE; apply/andb_idr/sAB.
 Qed.
-Implicit Arguments setIidPl [A B].
+Arguments setIidPl [A B].
 
 Lemma setIidPr A B : reflect (A :&: B = B) (B \subset A).
 Proof. by rewrite setIC; apply: setIidPl. Qed.
@@ -955,26 +955,26 @@ Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed.
 
 End setOps.
 
-Implicit Arguments set1P [T x a].
-Implicit Arguments set1_inj [T].
-Implicit Arguments set2P [T x a b].
-Implicit Arguments setIdP [T x pA pB].
-Implicit Arguments setIP [T x A B].
-Implicit Arguments setU1P [T x a B].
-Implicit Arguments setD1P [T x A b].
-Implicit Arguments setUP [T x A B].
-Implicit Arguments setDP [T x A B].
-Implicit Arguments cards1P [T A].
-Implicit Arguments setCP [T x A].
-Implicit Arguments setIidPl [T A B].
-Implicit Arguments setIidPr [T A B].
-Implicit Arguments setUidPl [T A B].
-Implicit Arguments setUidPr [T A B].
-Implicit Arguments setDidPl [T A B].
-Implicit Arguments subsetIP [T A B C].
-Implicit Arguments subUsetP [T A B C].
-Implicit Arguments subsetDP [T A B C].
-Implicit Arguments subsetD1P [T A B x].
+Arguments set1P [T x a].
+Arguments set1_inj [T].
+Arguments set2P [T x a b].
+Arguments setIdP [T x pA pB].
+Arguments setIP [T x A B].
+Arguments setU1P [T x a B].
+Arguments setD1P [T x A b].
+Arguments setUP [T x A B].
+Arguments setDP [T A B x].
+Arguments cards1P [T A].
+Arguments setCP [T x A].
+Arguments setIidPl [T A B].
+Arguments setIidPr [T A B].
+Arguments setUidPl [T A B].
+Arguments setUidPr [T A B].
+Arguments setDidPl [T A B].
+Arguments subsetIP [T A B C].
+Arguments subUsetP [T A B C].
+Arguments subsetDP [T A B C].
+Arguments subsetD1P [T A B x].
 Prenex Implicits set1 set1_inj.
 Prenex Implicits set1P set2P setU1P setD1P setIdP setIP setUP setDP.
 Prenex Implicits cards1P setCP setIidPl setIidPr setUidPl setUidPr setDidPl.
@@ -1018,7 +1018,7 @@ Proof. by rewrite cardsE cardX. Qed.
 
 End CartesianProd.
 
-Implicit Arguments setXP [x1 x2 fT1 fT2 A1 A2].
+Arguments setXP [fT1 fT2 A1 A2 x1 x2].
 Prenex Implicits setXP.
 
 Local Notation imset_def :=
@@ -1365,8 +1365,8 @@ Proof. by move=> sAB1 sAB2; rewrite -!imset2_pair imset2S. Qed.
 
 End FunImage.
 
-Implicit Arguments imsetP [aT rT f D y].
-Implicit Arguments imset2P [aT aT2 rT f2 D1 D2 y].
+Arguments imsetP [aT rT f D y].
+Arguments imset2P [aT aT2 rT f2 D1 D2 y].
 Prenex Implicits imsetP imset2P.
 
 Section BigOps.
@@ -1439,11 +1439,11 @@ Proof. by apply: partition_big => i Ai; apply/imsetP; exists i. Qed.
 
 End BigOps.
 
-Implicit Arguments big_setID [R idx aop I A].
-Implicit Arguments big_setD1 [R idx aop I A F].
-Implicit Arguments big_setU1 [R idx aop I A F].
-Implicit Arguments big_imset [R idx aop h I J A].
-Implicit Arguments partition_big_imset [R idx aop I J].
+Arguments big_setID [R idx aop I A].
+Arguments big_setD1 [R idx aop I] a [A F].
+Arguments big_setU1 [R idx aop I] a [A F].
+Arguments big_imset [R idx aop I J h A].
+Arguments partition_big_imset [R idx aop I J].
 
 Section Fun2Set1.
 
@@ -1499,7 +1499,7 @@ Proof. by move=> fK gK; apply: can2_in_imset_pre; apply: in1W. Qed.
 
 End CardFunImage.
 
-Implicit Arguments imset_injP [aT rT f D].
+Arguments imset_injP [aT rT f D].
 
 Lemma on_card_preimset (aT rT : finType) (f : aT -> rT) (R : pred rT) :
   {on R, bijective f} -> #|f @^-1: R| = #|R|.
@@ -1701,14 +1701,14 @@ Proof. by apply: setC_inj; rewrite !setC_bigcap bigcup_seq. Qed.
 
 End BigSetOps.
 
-Implicit Arguments bigcup_sup [T I P F].
-Implicit Arguments bigcup_max [T I U P F].
-Implicit Arguments bigcupP [T I x P F].
-Implicit Arguments bigcupsP [T I U P F].
-Implicit Arguments bigcap_inf [T I P F].
-Implicit Arguments bigcap_min [T I U P F].
-Implicit Arguments bigcapP [T I x P F].
-Implicit Arguments bigcapsP [T I U P F].
+Arguments bigcup_sup [T I] j [P F].
+Arguments bigcup_max [T I] j [U P F].
+Arguments bigcupP [T I x P F].
+Arguments bigcupsP [T I U P F].
+Arguments bigcap_inf [T I] j [P F].
+Arguments bigcap_min [T I] j [U P F].
+Arguments bigcapP [T I x P F].
+Arguments bigcapsP [T I U P F].
 Prenex Implicits bigcupP bigcupsP bigcapP bigcapsP.
 
 Section ImsetCurry.
@@ -2088,11 +2088,11 @@ End Transversals.
 
 End Partitions.
 
-Implicit Arguments trivIsetP [T P].
-Implicit Arguments big_trivIset_cond [T R idx op K E].
-Implicit Arguments set_partition_big_cond [T R idx op D K E].
-Implicit Arguments big_trivIset [T R idx op E].
-Implicit Arguments set_partition_big [T R idx op D E].
+Arguments trivIsetP [T P].
+Arguments big_trivIset_cond [T R idx op] P [K E].
+Arguments set_partition_big_cond [T R idx op] P [D K E].
+Arguments big_trivIset [T R idx op] P [E].
+Arguments set_partition_big [T R idx op] P [D E].
 
 Prenex Implicits cover trivIset partition pblock trivIsetP.
 
@@ -2141,7 +2141,7 @@ apply: (iffP forallP) => [minA | [PA minA] B].
   by move=> B PB sBA; have:= minA B; rewrite PB sBA /= eqb_id => /eqP.
 by apply/implyP=> sBA; apply/eqP; apply/eqP/idP=> [-> // | /minA]; apply.
 Qed.
-Implicit Arguments minsetP [P A].
+Arguments minsetP [P A].
 
 Lemma minsetp P A : minset P A -> P A.
 Proof. by case/minsetP. Qed.
@@ -2212,7 +2212,7 @@ Qed.
 
 End MaxSetMinSet.
 
-Implicit Arguments minsetP [T P A].
-Implicit Arguments maxsetP [T P A].
+Arguments minsetP [T P A].
+Arguments maxsetP [T P A].
 Prenex Implicits minset maxset minsetP maxsetP.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 719a267..1446fbd 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -820,13 +820,13 @@ End OpsTheory.
 
 Hint Resolve subxx_hint.
 
-Implicit Arguments pred0P [T P].
-Implicit Arguments pred0Pn [T P].
-Implicit Arguments subsetP [T A B].
-Implicit Arguments subsetPn [T A B].
-Implicit Arguments subset_eqP [T A B].
-Implicit Arguments card_uniqP [T s].
-Implicit Arguments properP [T A B].
+Arguments pred0P [T P].
+Arguments pred0Pn [T P].
+Arguments subsetP [T A B].
+Arguments subsetPn [T A B].
+Arguments subset_eqP [T A B].
+Arguments card_uniqP [T s].
+Arguments properP [T A B].
 Prenex Implicits pred0P pred0Pn subsetP subsetPn subset_eqP card_uniqP.
 
 (**********************************************************************)
@@ -919,14 +919,14 @@ Proof. by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if. Qed.
 
 End Quantifiers.
 
-Implicit Arguments forallP [T P].
-Implicit Arguments eqfunP [T rT f1 f2].
-Implicit Arguments forall_inP [T D P].
-Implicit Arguments eqfun_inP [T rT D f1 f2].
-Implicit Arguments existsP [T P].
-Implicit Arguments exists_eqP [T rT f1 f2].
-Implicit Arguments exists_inP [T D P].
-Implicit Arguments exists_eq_inP [T rT D f1 f2].
+Arguments forallP [T P].
+Arguments eqfunP [T rT f1 f2].
+Arguments forall_inP [T D P].
+Arguments eqfun_inP [T rT D f1 f2].
+Arguments existsP [T P].
+Arguments exists_eqP [T rT f1 f2].
+Arguments exists_inP [T D P].
+Arguments exists_eq_inP [T rT D f1 f2].
 
 Section Extrema.
 
@@ -1184,15 +1184,15 @@ Qed.
 End Image.
 
 Prenex Implicits codom iinv.
-Implicit Arguments imageP [T T' f A y].
-Implicit Arguments codomP [T T' f y].
+Arguments imageP [T T' f A y].
+Arguments codomP [T T' f y].
 
 Lemma flatten_imageP (aT : finType) (rT : eqType) A (P : pred aT) (y : rT) :
   reflect (exists2 x, x \in P & y \in A x) (y \in flatten [seq A x | x in P]).
 Proof.
 by apply: (iffP flatten_mapP) => [][x Px]; exists x; rewrite ?mem_enum in Px *.
 Qed.
-Implicit Arguments flatten_imageP [aT rT A P y].
+Arguments flatten_imageP [aT rT A P y].
 
 Section CardFunImage.
 
@@ -1240,7 +1240,7 @@ Qed.
 
 End CardFunImage.
 
-Implicit Arguments image_injP [T T' f A].
+Arguments image_injP [T T' f A].
 
 Section FinCancel.
 
@@ -1748,8 +1748,8 @@ Qed.
 
 End EnumRank.
 
-Implicit Arguments enum_val_inj [[T] [A] x1 x2].
-Implicit Arguments enum_rank_inj [[T] x1 x2].
+Arguments enum_val_inj {T A} [x1 x2].
+Arguments enum_rank_inj {T} [x1 x2].
 Prenex Implicits enum_val enum_rank.
 
 Lemma enum_rank_ord n i : enum_rank i = cast_ord (esym (card_ord n)) i.
@@ -1963,10 +1963,10 @@ Lemma lift0 (i : 'I_n') : lift ord0 i = i.+1 :> nat. Proof. by []. Qed.
 
 End OrdinalPos.
 
-Implicit Arguments ord0 [[n']].
-Implicit Arguments ord_max [[n']].
-Implicit Arguments inord [[n']].
-Implicit Arguments sub_ord [[n']].
+Arguments ord0 {n'}.
+Arguments ord_max {n'}.
+Arguments inord {n'}.
+Arguments sub_ord {n'}.
 
 (* Product of two fintypes which is a fintype *)
 Section ProdFinType.
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index 0aafc34..a3e6cac 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -198,7 +198,7 @@ Notation QuotType Q m := (@QuotType_pack _ Q m).
 Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id)
  (at level 0, format "[ 'quotType'  'of'  Q ]") : form_scope.
 
-Implicit Arguments repr [T qT].
+Arguments repr [T qT].
 Prenex Implicits repr.
 
 (************************)
@@ -248,7 +248,7 @@ Notation piE := (@equal_toE _ _).
 Canonical equal_to_pi T (qT : quotType T) (x : T) :=
   @EqualTo _ (\pi_qT x) (\pi x) (erefl _).
 
-Implicit Arguments EqualTo [T x equal_val].
+Arguments EqualTo [T x equal_val].
 Prenex Implicits EqualTo.
 
 Section Morphism.
@@ -276,11 +276,11 @@ Lemma pi_morph11 : \pi (h a) = hq (equal_val x). Proof. by rewrite !piE. Qed.
 
 End Morphism.
 
-Implicit Arguments pi_morph1 [T qT f fq].
-Implicit Arguments pi_morph2 [T qT g gq].
-Implicit Arguments pi_mono1 [T U qT p pq].
-Implicit Arguments pi_mono2 [T U qT r rq].
-Implicit Arguments pi_morph11 [T U qT qU h hq].
+Arguments pi_morph1 [T qT f fq].
+Arguments pi_morph2 [T qT g gq].
+Arguments pi_mono1 [T U qT p pq].
+Arguments pi_mono2 [T U qT r rq].
+Arguments pi_morph11 [T U qT qU h hq].
 Prenex Implicits pi_morph1 pi_morph2 pi_mono1 pi_mono2 pi_morph11.
 
 Notation "{pi_ Q a }" := (equal_to (\pi_Q a)) : quotient_scope.
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 4f3beb4..e649cbe 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -159,7 +159,7 @@ Qed.
 
 End Paths.
 
-Implicit Arguments pathP [T e x p].
+Arguments pathP [T e x p].
 Prenex Implicits pathP.
 
 Section EqPath.
@@ -687,9 +687,9 @@ Qed.
 
 End EqTrajectory.
 
-Implicit Arguments fpathP [T f x p].
-Implicit Arguments loopingP [T f x n].
-Implicit Arguments trajectP [T f x n y].
+Arguments fpathP [T f x p].
+Arguments loopingP [T f x n].
+Arguments trajectP [T f x n y].
 Prenex Implicits traject fpathP loopingP trajectP.
 
 Section UniqCycle.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 9494353..648737b 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -349,8 +349,8 @@ case/primeP=> _ min_p d_neq1; apply: (iffP idP) => [/min_p|-> //].
 by rewrite (negPf d_neq1) /= => /eqP.
 Qed.
 
-Implicit Arguments primeP [p].
-Implicit Arguments primePn [n].
+Arguments primeP [p].
+Arguments primePn [n].
 Prenex Implicits primePn primeP.
 
 Lemma prime_gt1 p : prime p -> 1 < p.
@@ -541,7 +541,7 @@ exists (pdiv n); rewrite pdiv_dvd pdiv_prime //; split=> //.
 by case: leqP npr_p => //; move/ltn_pdiv2_prime->; auto.
 Qed.
 
-Implicit Arguments primePns [n].
+Arguments primePns [n].
 Prenex Implicits primePns.
 
 Lemma pdivP n : n > 1 -> {p | prime p & p %| n}.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 5574892..a562879 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -780,8 +780,8 @@ End Sequences.
 
 Definition rev T (s : seq T) := nosimpl (catrev s [::]).
 
-Implicit Arguments nilP [T s].
-Implicit Arguments all_filterP [T a s].
+Arguments nilP [T s].
+Arguments all_filterP [T a s].
 
 Prenex Implicits size nilP head ohead behead last rcons belast.
 Prenex Implicits cat take drop rev rot rotr.
@@ -875,7 +875,7 @@ Qed.
 
 End Rev.
 
-Implicit Arguments revK [[T]].
+Arguments revK {T}.
 
 (* Equality and eqType for seq.                                          *)
 
@@ -1287,13 +1287,13 @@ Definition inE := (mem_seq1, in_cons, inE).
 
 Prenex Implicits mem_seq1 uniq undup index.
 
-Implicit Arguments eqseqP [T x y].
-Implicit Arguments hasP [T a s].
-Implicit Arguments hasPn [T a s].
-Implicit Arguments allP [T a s].
-Implicit Arguments allPn [T a s].
-Implicit Arguments nseqP [T n x y].
-Implicit Arguments count_memPn [T x s].
+Arguments eqseqP [T x y].
+Arguments hasP [T a s].
+Arguments hasPn [T a s].
+Arguments allP [T a s].
+Arguments allPn [T a s].
+Arguments nseqP [T n x y].
+Arguments count_memPn [T x s].
 Prenex Implicits eqseqP hasP hasPn allP allPn nseqP count_memPn.
 
 Section NthTheory.
@@ -1332,9 +1332,9 @@ Proof. by elim: s n => [|y s' IHs] [|n] /=; auto. Qed.
 Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x).
 Proof. by case: s. Qed.
 
-Implicit Arguments nthP [T s x].
-Implicit Arguments has_nthP [T a s].
-Implicit Arguments all_nthP [T a s].
+Arguments nthP [T s x].
+Arguments has_nthP [T a s].
+Arguments all_nthP [T a s].
 Prenex Implicits nthP has_nthP all_nthP.
 
 Definition bitseq := seq bool.
@@ -1576,9 +1576,9 @@ End PermSeq.
 Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
 Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2).
 
-Implicit Arguments perm_eqP [T s1 s2].
-Implicit Arguments perm_eqlP [T s1 s2].
-Implicit Arguments perm_eqrP [T s1 s2].
+Arguments perm_eqP [T s1 s2].
+Arguments perm_eqlP [T s1 s2].
+Arguments perm_eqrP [T s1 s2].
 Prenex Implicits perm_eq perm_eqP perm_eqlP perm_eqrP.
 Hint Resolve perm_eq_refl.
 
@@ -1853,7 +1853,7 @@ Proof. by case/subseqP=> m _ -> Us2; apply: mask_uniq. Qed.
 End Subseq.
 
 Prenex Implicits subseq.
-Implicit Arguments subseqP [T s1 s2].
+Arguments subseqP [T s1 s2].
 
 Hint Resolve subseq_refl.
 
@@ -2029,7 +2029,7 @@ Qed.
 
 End FilterSubseq.
 
-Implicit Arguments subseq_uniqP [T s1 s2].
+Arguments subseq_uniqP [T s1 s2].
 
 Section EqMap.
 
@@ -2097,7 +2097,7 @@ Proof. by apply: map_inj_in_uniq; apply: in2W. Qed.
 
 End EqMap.
 
-Implicit Arguments mapP [T1 T2 f s y].
+Arguments mapP [T1 T2 f s y].
 Prenex Implicits mapP.
 
 Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) :
@@ -2289,7 +2289,7 @@ Qed.
 
 End MakeEqSeq.
 
-Implicit Arguments perm_eq_iotaP [[T] [s] [t]].
+Arguments perm_eq_iotaP {T s t}.
 
 Section FoldRight.
 
@@ -2663,7 +2663,7 @@ elim: A => /= [|s A /iffP IH_A]; [by right; case | rewrite mem_cat].
 have [s_x|s'x] := @idP (x \in s); first by left; exists s; rewrite ?mem_head.
 by apply: IH_A => [[t] | [t /predU1P[->|]]]; exists t; rewrite // mem_behead.
 Qed.
-Implicit Arguments flattenP [A x].
+Arguments flattenP [A x].
 
 Lemma flatten_mapP (A : S -> seq T) s y :
   reflect (exists2 x, x \in s & y \in A x) (y \in flatten (map A s)).
@@ -2674,8 +2674,8 @@ Qed.
 
 End EqFlatten.
 
-Implicit Arguments flattenP [T A x].
-Implicit Arguments flatten_mapP [S T A s y].
+Arguments flattenP [T A x].
+Arguments flatten_mapP [S T A s y].
 
 Lemma perm_undup_count (T : eqType) (s : seq T) :
   perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 1c16140..0e5899a 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -174,7 +174,7 @@ Qed.
 Canonical nat_eqMixin := EqMixin eqnP.
 Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
 
-Implicit Arguments eqnP [x y].
+Arguments eqnP [x y].
 Prenex Implicits eqnP.
 
 Lemma eqnE : eqn = eq_op. Proof. by []. Qed.
@@ -394,7 +394,7 @@ apply: (iffP idP); last by elim: n / => // n _ /leq_trans->.
 elim: n => [|n IHn]; first by case: m.
 by rewrite leq_eqVlt ltnS => /predU1P[<- // | /IHn]; right.
 Qed.
-Implicit Arguments leP [m n].
+Arguments leP [m n].
 
 Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat.
 Proof.
@@ -411,7 +411,7 @@ Qed.
 
 Lemma ltP m n : reflect (m < n)%coq_nat (m < n).
 Proof. exact leP. Qed.
-Implicit Arguments ltP [m n].
+Arguments ltP [m n].
 
 Lemma lt_irrelevance m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat.
 Proof. exact: (@le_irrelevance m.+1). Qed.
@@ -925,19 +925,19 @@ Proof. by rewrite eqn_leq !leq_mul2r -orb_andr -eqn_leq. Qed.
 
 Lemma leq_pmul2l m n1 n2 : 0 < m -> (m * n1 <= m * n2) = (n1 <= n2).
 Proof. by move/prednK=> <-; rewrite leq_mul2l. Qed.
-Implicit Arguments leq_pmul2l [m n1 n2].
+Arguments leq_pmul2l [m n1 n2].
 
 Lemma leq_pmul2r m n1 n2 : 0 < m -> (n1 * m <= n2 * m) = (n1 <= n2).
 Proof. by move/prednK <-; rewrite leq_mul2r. Qed.
-Implicit Arguments leq_pmul2r [m n1 n2].
+Arguments leq_pmul2r [m n1 n2].
 
 Lemma eqn_pmul2l m n1 n2 : 0 < m -> (m * n1 == m * n2) = (n1 == n2).
 Proof. by move/prednK <-; rewrite eqn_mul2l. Qed.
-Implicit Arguments eqn_pmul2l [m n1 n2].
+Arguments eqn_pmul2l [m n1 n2].
 
 Lemma eqn_pmul2r m n1 n2 : 0 < m -> (n1 * m == n2 * m) = (n1 == n2).
 Proof. by move/prednK <-; rewrite eqn_mul2r. Qed.
-Implicit Arguments eqn_pmul2r [m n1 n2].
+Arguments eqn_pmul2r [m n1 n2].
 
 Lemma ltn_mul2l m n1 n2 : (m * n1 < m * n2) = (0 < m) && (n1 < n2).
 Proof. by rewrite lt0n !ltnNge leq_mul2l negb_or. Qed.
@@ -947,11 +947,11 @@ Proof. by rewrite lt0n !ltnNge leq_mul2r negb_or. Qed.
 
 Lemma ltn_pmul2l m n1 n2 : 0 < m -> (m * n1 < m * n2) = (n1 < n2).
 Proof. by move/prednK <-; rewrite ltn_mul2l. Qed.
-Implicit Arguments ltn_pmul2l [m n1 n2].
+Arguments ltn_pmul2l [m n1 n2].
 
 Lemma ltn_pmul2r m n1 n2 : 0 < m -> (n1 * m < n2 * m) = (n1 < n2).
 Proof. by move/prednK <-; rewrite ltn_mul2r. Qed.
-Implicit Arguments ltn_pmul2r [m n1 n2].
+Arguments ltn_pmul2r [m n1 n2].
 
 Lemma ltn_Pmull m n : 1 < n -> 0 < m -> m < n * m.
 Proof. by move=> lt1n m_gt0; rewrite -{1}[m]mul1n ltn_pmul2r. Qed.
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 7023bb4..e06bd38 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -266,8 +266,8 @@ Proof. by rewrite -existsb_tnth; apply: existsP. Qed.
 
 End TupleQuantifiers.
 
-Implicit Arguments all_tnthP [n T a t].
-Implicit Arguments has_tnthP [n T a t].
+Arguments all_tnthP [n T a t].
+Arguments has_tnthP [n T a t].
 
 Section EqTuple.