diff options
Diffstat (limited to 'mathcomp/character/character.v')
| -rw-r--r-- | mathcomp/character/character.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index e522924..6752623 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -390,8 +390,8 @@ Qed. End StandardRepresentation. -Arguments grepr0 [R gT G]. -Prenex Implicits grepr0 dadd_grepr. +Arguments grepr0 {R gT G}. +Prenex Implicits dadd_grepr. Section Char. @@ -924,7 +924,7 @@ Canonical char_semiringPred := SemiringPred mul_char. End IsChar. Prenex Implicits character. -Arguments char_reprP [gT G phi]. +Arguments char_reprP {gT G phi}. Section AutChar. @@ -2554,7 +2554,7 @@ Qed. End DerivedGroup. -Arguments irr_prime_injP [gT G i]. +Arguments irr_prime_injP {gT G i}. (* Determinant characters and determinential order. *) Section DetOrder. |