diff options
| author | Cyril Cohen | 2020-06-09 01:16:56 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-09 04:45:15 +0200 |
| commit | 8006cbf40eeb017aacb3ecaa8c4538f9a5aaa3bf (patch) | |
| tree | 805fe2e3ff31c9741ae0ded3cd7ab24b7068f60d /mathcomp/character | |
| parent | 6784363d60493b8ec154bbf1e827ec677d6b5921 (diff) | |
fix coq 8.12 warnings
Diffstat (limited to 'mathcomp/character')
| -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"). |