diff options
| author | Cyril Cohen | 2020-11-20 03:10:59 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-20 03:10:59 +0100 |
| commit | 7c47bab45686e90ee50e6c7eaae3230cb7ce9e53 (patch) | |
| tree | 3e90f47d229669b376a967c63b3aa9bb6ad89beb /mathcomp/algebra/poly.v | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
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 e3de209..4ddb8cd 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 <:]. |