4 files changed, 11 insertions, 11 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 4487ab4..7473ed7 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -460,7 +460,7 @@ Notation "x |-> y" := (FunDelta x y)
    format "'[hv' x '/ '  |->  y ']'") : fun_delta_scope.
 
 Delimit Scope fun_delta_scope with FUN_DELTA.
-Arguments app_fdelta _ _%type _%FUN_DELTA _ _.
+Arguments app_fdelta {aT rT%type} df%FUN_DELTA f z.
 
 Notation "[ 'fun' z : T => F 'with' d1 , .. , dn ]" :=
   (SimplFunDelta (fun z : T =>
@@ -603,7 +603,7 @@ 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}.
+Arguments val_inj {T P sT} [x1 x2].
 Prenex Implicits val insubd.
 
 Local Notation inlined_sub_rect :=
@@ -779,7 +779,7 @@ Proof. by case/andP. Qed.
 
 End ProdEqType.
 
-Arguments pair_eq {T1 T2} _ _ /.
+Arguments pair_eq {T1 T2} u v /.
 Arguments pair_eqP {T1 T2}.
 
 Definition predX T1 T2 (p1 : pred T1) (p2 : pred T2) :=
@@ -805,7 +805,7 @@ Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin.
 
 End OptionEqType.
 
-Arguments opt_eq {T} !_ !_.
+Arguments opt_eq {T} !u !v.
 
 Section TaggedAs.
 
@@ -851,7 +851,7 @@ Proof. by rewrite -tag_eqE /tag_eq eqxx tagged_asE. Qed.
 
 End TagEqType.
 
-Arguments tag_eq {I T_} !_ !_.
+Arguments tag_eq {I T_} !u !v.
 Arguments tag_eqP {I T_ x y}.
 
 Section SumEqType.
@@ -875,5 +875,5 @@ Lemma sum_eqE : sum_eq = eq_op. Proof. by []. Qed.
 
 End SumEqType.
 
-Arguments sum_eq {T1 T2} !_ !_.
+Arguments sum_eq {T1 T2} !u !v.
 Arguments sum_eqP {T1 T2 x y}.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 3fd10fa..4ad02c6 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -130,7 +130,7 @@ Delimit Scope set_scope with SET.
 Bind Scope set_scope with set_type.
 Bind Scope set_scope with set_of.
 Open Scope set_scope.
-Arguments finfun_of_set _ _%SET.
+Arguments finfun_of_set {T} A%SET.
 
 Notation "{ 'set' T }" := (set_of (Phant T))
   (at level 0, format "{ 'set'  T }") : type_scope.
@@ -955,7 +955,7 @@ Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed.
 End setOps.
 
 Arguments set1P {T x a}.
-Arguments set1_inj {T}.
+Arguments set1_inj {T} [x1 x2].
 Arguments set2P {T x a b}.
 Arguments setIdP {T x pA pB}.
 Arguments setIP {T x A B}.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 4b2952f..d4f564f 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -1760,7 +1760,7 @@ Qed.
 
 End EnumRank.
 
-Arguments enum_val_inj {T A} [x1 x2].
+Arguments enum_val_inj {T A} [i1 i2] : rename.
 Arguments enum_rank_inj {T} [x1 x2].
 Prenex Implicits enum_val enum_rank.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index b24da11..b8388f0 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.
 
-Arguments eqn !_ !_.
+Arguments eqn !m !n.
 Arguments eqnP {x y}.
 
 Lemma eqnE : eqn = eq_op. Proof. by []. Qed.
@@ -1454,7 +1454,7 @@ Qed.
 Canonical bin_nat_eqMixin := EqMixin eq_binP.
 Canonical bin_nat_eqType := Eval hnf in EqType N bin_nat_eqMixin.
 
-Arguments N.eqb !_ !_.
+Arguments N.eqb !n !m.
 
 Section NumberInterpretation.