aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/character/vcharacter.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/character/vcharacter.v')
-rw-r--r--mathcomp/character/vcharacter.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 97ad828..5c9ca9b 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -709,7 +709,7 @@ End MoreVchar.
Definition dirr (gT : finGroupType) (B : {set gT}) : pred_class :=
[pred f : 'CF(B) | (f \in irr B) || (- f \in irr B)].
-Implicit Arguments dirr [[gT]].
+Arguments dirr {gT}.
Section Norm1vchar.