diff options
| author | affeldt-aist | 2020-11-20 17:55:19 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-20 17:55:19 +0900 |
| commit | b4cdd47bcd7f2b2f9033ee00b7412570b07b8808 (patch) | |
| tree | 63eaf93913a44ffc2d21c705640af01cdd3bbd17 /mathcomp/algebra/poly.v | |
| parent | 3bb1ccc63170e3e71ef9d5b62758b6fdb1c4371c (diff) | |
| parent | 7c47bab45686e90ee50e6c7eaae3230cb7ce9e53 (diff) | |
Merge pull request #663 from CohenCyril/clean_head
Using Arguments / to deal with volatile definitions
Diffstat (limited to 'mathcomp/algebra/poly.v')
| -rw-r--r-- | mathcomp/algebra/poly.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index c413171..21e8ada 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -140,7 +140,7 @@ Lemma poly_inj : injective polyseq. Proof. exact: val_inj. Qed. Definition poly_of of phant R := polynomial. Identity Coercion type_poly_of : poly_of >-> polynomial. -Definition coefp_head h i (p : poly_of (Phant R)) := let: tt := h in p`_i. +Definition coefp i (p : poly_of (Phant R)) := p`_i. End Polynomial. @@ -150,9 +150,8 @@ Bind Scope ring_scope with poly_of. Bind Scope ring_scope with polynomial. Arguments polyseq {R} p%R. Arguments poly_inj {R} [p1%R p2%R] : rename. -Arguments coefp_head {R} h i%N p%R. +Arguments coefp {R} i%N / p%R. Notation "{ 'poly' T }" := (poly_of (Phant T)). -Notation coefp i := (coefp_head tt i). Definition poly_countMixin (R : countRingType) := [countMixin of polynomial R by <:]. |