diff options
Diffstat (limited to 'mathcomp/algebra/poly.v')
| -rw-r--r-- | mathcomp/algebra/poly.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 34174bf..929c313 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -146,9 +146,9 @@ End Polynomial. (* directives take effect. *) Bind Scope ring_scope with poly_of. Bind Scope ring_scope with polynomial. -Arguments polyseq _ _%R. -Arguments poly_inj _ _%R _%R _. -Arguments coefp_head _ _ _%N _%R. +Arguments polyseq {R} p%R. +Arguments poly_inj {R} [p1%R p2%R] : rename. +Arguments coefp_head {R} h i%N p%R. Notation "{ 'poly' T }" := (poly_of (Phant T)). Notation coefp i := (coefp_head tt i). @@ -2430,7 +2430,7 @@ Qed. End MapFieldPoly. -Arguments map_poly_inj {F R} f [x1 x2]. +Arguments map_poly_inj {F R} f [p1 p2] : rename. Section MaxRoots. |