diff options
| author | Georges Gonthier | 2018-12-04 13:27:53 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-04 13:27:53 +0100 |
| commit | e99b8b9695cdb53492e63077cb0dd551c4a06dc3 (patch) | |
| tree | 9af429f5d53b30de0c44e11ed651403289f39108 /mathcomp/algebra/poly.v | |
| parent | 03ad994dfee48e1a7b2b7091c45dfdcf4402f826 (diff) | |
| parent | 8c82657e7692049dde4a4c44a2ea53d0c4fa7cb5 (diff) | |
Merge pull request #253 from anton-trunov/arguments
Document parameter names whenever possible
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. |