fix coq 8.12 warnings

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").