diff options
Diffstat (limited to 'mathcomp/character/classfun.v')
| -rw-r--r-- | mathcomp/character/classfun.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index fc19eba..9c4557a 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -98,16 +98,16 @@ Delimit Scope cfun_scope with CF. Reserved Notation "''CF' ( G , A )" (at level 8, format "''CF' ( G , A )"). Reserved Notation "''CF' ( G )" (at level 8, format "''CF' ( G )"). Reserved Notation "''1_' G" (at level 8, G at level 2, format "''1_' G"). -Reserved Notation "''Res[' H , G ]" (at level 8, only parsing). +Reserved Notation "''Res[' H , G ]" (at level 8). (* only parsing *) Reserved Notation "''Res[' H ]" (at level 8, format "''Res[' H ]"). -Reserved Notation "''Res'" (at level 8, only parsing). -Reserved Notation "''Ind[' G , H ]" (at level 8, only parsing). -Reserved Notation "''Ind[' G ]" (at level 8, format "''Ind[' G ]"). -Reserved Notation "''Ind'" (at level 8, only parsing). -Reserved Notation "'[ phi , psi ]_ G" (at level 2, only parsing). +Reserved Notation "''Res'" (at level 8). (* only parsing *) +Reserved Notation "''Ind[' G , H ]" (at level 8). (* only parsing *) +Reserved Notation "''Ind[' G ]" (at level 8). (* only "''Ind[' G ]" *) +Reserved Notation "''Ind'" (at level 8). (* only parsing *) +Reserved Notation "'[ phi , psi ]_ G" (at level 2). (* only parsing *) Reserved Notation "'[ phi , psi ]" (at level 2, format "'[hv' ''[' phi , '/ ' psi ] ']'"). -Reserved Notation "'[ phi ]_ G" (at level 2, only parsing). +Reserved Notation "'[ phi ]_ G" (at level 2). (* only parsing *) Reserved Notation "'[ phi ]" (at level 2, format "''[' phi ]"). Reserved Notation "phi ^u" (at level 3, format "phi ^u"). |