3 files changed, 6 insertions, 6 deletions
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 8a65f2b..ad2388a 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -260,7 +260,7 @@ Qed.
 Prenex Implicits alg_integral.
 
 Import DefaultKeying GRing.DefaultPred.
-Arguments map_poly_inj {F R} f [x1 x2].
+Arguments map_poly_inj {F R} f [p1 p2].
 
 Theorem Fundamental_Theorem_of_Algebraics :
   {L : closedFieldType &
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index 1ae025b..0440653 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -54,18 +54,18 @@ Proof. by split=> /andP[]. Qed.
 
 Notation cps T := ((T -> fF) -> fF).
 Definition ret T1 : T1 -> cps T1 := fun x k => k x.
-Arguments ret T1 x k /.
+Arguments ret {T1} x k /.
 
 Definition bind T1 T2 (x : cps T1) (f : T1 -> cps T2) : cps T2 :=
   fun k => x (fun x => f x k).
-Arguments bind T1 T2 x f k /.
+Arguments bind {T1 T2} x f k /.
 Notation "''let' x <- y ; z" :=
   (bind y (fun x => z)) (at level 99, x at level 0, y at level 0,
     format "'[hv' ''let'  x  <-  y ;  '/' z ']'").
 
 Definition cpsif T (c : fF) (t : T) (e : T) : cps T :=
   fun k => GRing.If c (k t) (k e).
-Arguments cpsif T c t e k /.
+Arguments cpsif {T} c t e k /.
 Notation "''if' c1 'then' c2 'else' c3" := (cpsif c1%T c2%T c3%T)
   (at level 200, right associativity, format
 "'[hv   ' ''if'  c1  '/' '[' 'then'  c2  ']' '/' '[' 'else'  c3 ']' ']'").
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index 0410e55..7e86d3c 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -620,8 +620,8 @@ End FalgebraTheory.
 Delimit Scope aspace_scope with AS.
 Bind Scope aspace_scope with aspace.
 Bind Scope aspace_scope with aspace_of.
-Arguments asval _ _ _%AS.
-Arguments clone_aspace _ _ _%VS _%AS _ _.
+Arguments asval {K aT} a%AS.
+Arguments clone_aspace [K aT U%VS A%AS algU] _.
 
 Notation "{ 'aspace' T }" := (aspace_of (Phant T)) : type_scope.
 Notation "A * B" := (prodv A B) : vspace_scope.