diff options
| author | Cyril Cohen | 2018-11-24 17:58:35 +0100 |
|---|---|---|
| committer | GitHub | 2018-11-24 17:58:35 +0100 |
| commit | add6e85884691faef1bf8742e803374815672cc2 (patch) | |
| tree | 2ffb41f5afa11a147989c8efcc1dcb295ae2ed2b /mathcomp/character/character.v | |
| parent | 967088a6f87405a93ce21971392c58996df8c99f (diff) | |
| parent | f049e51c39077a025907ea87c08178dad1841801 (diff) | |
Merge pull request #249 from anton-trunov/prenex-implicits
Merge Arguments and Prenex Implicits
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. |