From 2525c33691e25f837b7dca31d4c702199b3dbc5d Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Sun, 4 Mar 2018 16:57:06 -0800 Subject: Change deprecated Arguments Scope to Arguments --- mathcomp/algebra/matrix.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/algebra/matrix.v') diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index b54e586..ec9fcc5 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -2660,7 +2660,7 @@ Coercion GLval ph (u : GLtype ph) : 'M[R]_n.-1.+1 := End FinUnitMatrix. Bind Scope group_scope with GLtype. -Arguments Scope GLval [nat_scope _ _ group_scope]. +Arguments GLval _%N _ _ _%g. Prenex Implicits GLval. Notation "{ ''GL_' n [ R ] }" := (GLtype n (Phant R)) -- cgit v1.2.3