aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/character/inertia.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/character/inertia.v
parent6f075b64b936de9ee4fa79ea4dc1d2fb9b9cf2c8 (diff)
Change deprecated Arguments Scope to Arguments
Diffstat (limited to 'mathcomp/character/inertia.v')
-rw-r--r--mathcomp/character/inertia.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 7d4a84c..ffa9696 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -567,8 +567,8 @@ Qed.
End Inertia.
-Arguments Scope inertia [_ group_scope cfun_scope].
-Arguments Scope cfclass [_ group_scope cfun_scope group_scope].
+Arguments inertia _ _%g _%CF.
+Arguments cfclass _ _%g _%CF _%g.
Arguments conjg_Iirr_inj [gT H] y [x1 x2].
Notation "''I[' phi ] " := (inertia phi) : group_scope.