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

Merge Arguments and Prenex Implicits

13 files changed, 115 insertions, 133 deletions

diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index 9e7c77f..baa7231 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -562,8 +562,8 @@ Export Countable.Exports.
 
 Definition unpickle T := Countable.unpickle (Countable.class T).
 Definition pickle T := Countable.pickle (Countable.class T).
-Arguments unpickle [T].
-Prenex Implicits pickle unpickle.
+Arguments unpickle {T}.
+Prenex Implicits pickle.
 
 Section CountableTheory.
 
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 6565ddf..ed1eedf 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -302,8 +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.
-Arguments dvdnP [d m].
-Prenex Implicits dvdnP.
+Arguments dvdnP {d m}.
 
 Lemma dvdn0 d : d %| 0.
 Proof. by case: d. Qed.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 76b0521..4487ab4 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -171,7 +171,7 @@ Proof. by []. Qed.
 
 Lemma eqP T : Equality.axiom (@eq_op T).
 Proof. by case: T => ? []. Qed.
-Arguments eqP [T x y].
+Arguments eqP {T x y}.
 
 Delimit Scope eq_scope with EQ.
 Open Scope eq_scope.
@@ -254,8 +254,8 @@ Proof. by rewrite eq_sym; apply: ifN. Qed.
 
 End Contrapositives.
 
-Arguments memPn [T1 A x].
-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.
@@ -363,10 +363,10 @@ Proof. by case: eqP; [left | right]. Qed.
 
 End EqPred.
 
-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.
+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.
 
 Notation "[ 'predU1' x & A ]" := (predU1 x [mem A])
   (at level 0, format "[ 'predU1'  x  &  A ]") : fun_scope.
@@ -597,14 +597,14 @@ Qed.
 End SubType.
 
 Arguments SubType [T P].
-Arguments Sub [T P s].
-Arguments vrefl [T P].
-Arguments vrefl_rect [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 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.
+Arguments val_inj {T P sT}.
+Prenex Implicits val insubd.
 
 Local Notation inlined_sub_rect :=
   (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px).
@@ -646,8 +646,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).
-Arguments innew [T nT].
-Prenex Implicits innew.
+Arguments innew {T nT}.
 
 Lemma innew_val T nT : cancel val (@innew T nT).
 Proof. by move=> u; apply: val_inj; apply: SubK. Qed.
@@ -737,8 +736,7 @@ Proof. by []. Qed.
 
 End SubEqType.
 
-Arguments val_eqP [T P sT x y].
-Prenex Implicits val_eqP.
+Arguments val_eqP {T P sT x y}.
 
 Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T)
   (at level 0, format "[ 'eqMixin'  'of'  T  'by'  <: ]") : form_scope.
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 8b85320..9929e82 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)).
 
-Arguments familyP [aT rT pT F f].
-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.
 
-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 baf5efe..c534b7b 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.
 
-Arguments dfsP [T g x y].
-Arguments connectP [T e x y].
-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)).
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 6cff46e..3fd10fa 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -243,8 +243,7 @@ End BasicSetTheory.
 
 Definition inE := (in_set, inE).
 
-Arguments set0 [T].
-Prenex Implicits set0.
+Arguments set0 {T}.
 Hint Resolve in_setT.
 
 Notation "[ 'set' : T ]" := (setTfor (Phant T))
@@ -827,7 +826,7 @@ Proof.
 apply: (iffP subsetP) => [sAB | <- x /setIP[] //].
 by apply/setP=> x; rewrite inE; apply/andb_idr/sAB.
 Qed.
-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,29 +954,27 @@ Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed.
 
 End setOps.
 
-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.
+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.
 Hint Resolve subsetT_hint.
 
 Section setOpsAlgebra.
@@ -1018,8 +1015,7 @@ Proof. by rewrite cardsE cardX. Qed.
 
 End CartesianProd.
 
-Arguments setXP [fT1 fT2 A1 A2 x1 x2].
-Prenex Implicits setXP.
+Arguments setXP {fT1 fT2 A1 A2 x1 x2}.
 
 Local Notation imset_def :=
   (fun (aT rT : finType) f mD => [set y in @image_mem aT rT f mD]).
@@ -1365,9 +1361,8 @@ Proof. by move=> sAB1 sAB2; rewrite -!imset2_pair imset2S. Qed.
 
 End FunImage.
 
-Arguments imsetP [aT rT f D y].
-Arguments imset2P [aT aT2 rT f2 D1 D2 y].
-Prenex Implicits imsetP imset2P.
+Arguments imsetP {aT rT f D y}.
+Arguments imset2P {aT aT2 rT f2 D1 D2 y}.
 
 Section BigOps.
 
@@ -1499,7 +1494,7 @@ Proof. by move=> fK gK; apply: can2_in_imset_pre; apply: in1W. Qed.
 
 End CardFunImage.
 
-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|.
@@ -1703,13 +1698,12 @@ End BigSetOps.
 
 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 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.
+Arguments bigcapP {T I x P F}.
+Arguments bigcapsP {T I U P F}.
 
 Section ImsetCurry.
 
@@ -2088,13 +2082,13 @@ End Transversals.
 
 End Partitions.
 
-Arguments trivIsetP [T P].
+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.
+Prenex Implicits cover trivIset partition pblock.
 
 Lemma partition_partition (T : finType) (D : {set T}) P Q :
     partition P D -> partition Q P ->
@@ -2141,7 +2135,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.
-Arguments minsetP [P A].
+Arguments minsetP {P A}.
 
 Lemma minsetp P A : minset P A -> P A.
 Proof. by case/minsetP. Qed.
@@ -2212,7 +2206,7 @@ Qed.
 
 End MaxSetMinSet.
 
-Arguments minsetP [T P A].
-Arguments maxsetP [T P A].
-Prenex Implicits minset maxset minsetP maxsetP.
+Arguments minsetP {T P A}.
+Arguments maxsetP {T P A}.
+Prenex Implicits minset maxset.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 8848999..4b2952f 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -820,14 +820,13 @@ End OpsTheory.
 
 Hint Resolve subxx_hint.
 
-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.
+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}.
 
 (**********************************************************************)
 (*                                                                    *)
@@ -927,14 +926,14 @@ Proof. by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if. Qed.
 
 End Quantifiers.
 
-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].
+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}.
 
 Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view))
   (at level 4, right associativity, format "''exists_in_' view").
@@ -1197,15 +1196,15 @@ Qed.
 End Image.
 
 Prenex Implicits codom iinv.
-Arguments imageP [T T' f A y].
-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.
-Arguments flatten_imageP [aT rT A P y].
+Arguments flatten_imageP {aT rT A P y}.
 
 Section CardFunImage.
 
@@ -1253,7 +1252,7 @@ Qed.
 
 End CardFunImage.
 
-Arguments image_injP [T T' f A].
+Arguments image_injP {T T' f A}.
 
 Section FinCancel.
 
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index 16709ee..1475d55 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -198,8 +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.
 
-Arguments repr [T qT].
-Prenex Implicits repr.
+Arguments repr {T qT}.
 
 (************************)
 (* Exporting the theory *)
@@ -248,8 +247,7 @@ Notation piE := (@equal_toE _ _).
 Canonical equal_to_pi T (qT : quotType T) (x : T) :=
   @EqualTo _ (\pi_qT x) (\pi x) (erefl _).
 
-Arguments EqualTo [T x equal_val].
-Prenex Implicits EqualTo.
+Arguments EqualTo {T x equal_val}.
 
 Section Morphism.
 
@@ -276,12 +274,11 @@ Lemma pi_morph11 : \pi (h a) = hq (equal_val x). Proof. by rewrite !piE. Qed.
 
 End Morphism.
 
-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.
+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}.
 
 Notation "{pi_ Q a }" := (equal_to (\pi_Q a)) : quotient_scope.
 Notation "{pi a }" := (equal_to (\pi a)) : quotient_scope.
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 94873a8..dd67256 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -159,8 +159,7 @@ Qed.
 
 End Paths.
 
-Arguments pathP [T e x p].
-Prenex Implicits pathP.
+Arguments pathP {T e x p}.
 
 Section EqPath.
 
@@ -687,10 +686,10 @@ Qed.
 
 End EqTrajectory.
 
-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.
+Arguments fpathP {T f x p}.
+Arguments loopingP {T f x n}.
+Arguments trajectP {T f x n y}.
+Prenex Implicits traject.
 
 Section UniqCycle.
 
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 4bbea2a..02064c3 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -349,9 +349,8 @@ case/primeP=> _ min_p d_neq1; apply: (iffP idP) => [/min_p|-> //].
 by rewrite (negPf d_neq1) /= => /eqP.
 Qed.
 
-Arguments primeP [p].
-Arguments primePn [n].
-Prenex Implicits primePn primeP.
+Arguments primeP {p}.
+Arguments primePn {n}.
 
 Lemma prime_gt1 p : prime p -> 1 < p.
 Proof. by case/primeP. Qed.
@@ -541,8 +540,7 @@ exists (pdiv n); rewrite pdiv_dvd pdiv_prime //; split=> //.
 by case: leqP npr_p => //; move/ltn_pdiv2_prime->; auto.
 Qed.
 
-Arguments primePns [n].
-Prenex Implicits primePns.
+Arguments primePns {n}.
 
 Lemma pdivP n : n > 1 -> {p | prime p & p %| n}.
 Proof. by move=> lt1n; exists (pdiv n); rewrite ?pdiv_dvd ?pdiv_prime. Qed.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 9c13df3..ba1f969 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -786,12 +786,12 @@ End Sequences.
 
 Definition rev T (s : seq T) := nosimpl (catrev s [::]).
 
-Arguments nilP [T s].
-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 size head ohead behead last rcons belast.
 Prenex Implicits cat take drop rev rot rotr.
-Prenex Implicits find count nth all has filter all_filterP.
+Prenex Implicits find count nth all has filter.
 
 Notation count_mem x := (count (pred_of_simpl (pred1 x))).
 
@@ -1354,10 +1354,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.
 
-Arguments nthP [T s x].
-Arguments has_nthP [T a s].
-Arguments all_nthP [T a s].
-Prenex Implicits nthP has_nthP all_nthP.
+Arguments nthP {T s x}.
+Arguments has_nthP {T a s}.
+Arguments all_nthP {T a s}.
 
 Definition bitseq := seq bool.
 Canonical bitseq_eqType := Eval hnf in [eqType of bitseq].
@@ -1598,10 +1597,10 @@ 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).
 
-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.
+Arguments perm_eqP {T s1 s2}.
+Arguments perm_eqlP {T s1 s2}.
+Arguments perm_eqrP {T s1 s2}.
+Prenex Implicits perm_eq.
 Hint Resolve perm_eq_refl.
 
 Section RotrLemmas.
@@ -1875,7 +1874,7 @@ Proof. by case/subseqP=> m _ -> Us2; apply: mask_uniq. Qed.
 End Subseq.
 
 Prenex Implicits subseq.
-Arguments subseqP [T s1 s2].
+Arguments subseqP {T s1 s2}.
 
 Hint Resolve subseq_refl.
 
@@ -2119,8 +2118,7 @@ Proof. by apply: map_inj_in_uniq; apply: in2W. Qed.
 
 End EqMap.
 
-Arguments mapP [T1 T2 f s y].
-Prenex Implicits mapP.
+Arguments mapP {T1 T2 f s y}.
 
 Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) :
   {f | uniq s -> size fs = size s -> map f s = fs}.
@@ -2685,7 +2683,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.
-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)).
@@ -2696,8 +2694,8 @@ Qed.
 
 End EqFlatten.
 
-Arguments flattenP [T A x].
-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 78d50b6..b24da11 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -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.
-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.
-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.
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 38e3dbe..9154eb5 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.
 
-Arguments all_tnthP [n T a t].
-Arguments has_tnthP [n T a t].
+Arguments all_tnthP {n T a t}.
+Arguments has_tnthP {n T a t}.
 
 Section EqTuple.