aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/algebra/poly.v
diff options
context:
space:
mode:
authorJasper Hugunin2018-03-04 16:57:06 -0800
committerJasper Hugunin2018-03-04 16:57:06 -0800
commit2525c33691e25f837b7dca31d4c702199b3dbc5d (patch)
tree7937f252a0818909c715ccc20f3611a4f5c482d5 /mathcomp/algebra/poly.v
parent6f075b64b936de9ee4fa79ea4dc1d2fb9b9cf2c8 (diff)
Change deprecated Arguments Scope to Arguments
Diffstat (limited to 'mathcomp/algebra/poly.v')
-rw-r--r--mathcomp/algebra/poly.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 409930c..f34ca2d 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 Scope polyseq [_ ring_scope].
-Arguments Scope poly_inj [_ ring_scope ring_scope _].
-Arguments Scope coefp_head [_ _ nat_scope ring_scope _].
+Arguments polyseq _ _%R.
+Arguments poly_inj _ _%R _%R _.
+Arguments coefp_head _ _ _%N _%R.
Notation "{ 'poly' T }" := (poly_of (Phant T)).
Notation coefp i := (coefp_head tt i).