From 8006cbf40eeb017aacb3ecaa8c4538f9a5aaa3bf Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 9 Jun 2020 01:16:56 +0200
Subject: fix coq 8.12 warnings

---
 mathcomp/character/classfun.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'mathcomp/character')

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").
 
-- 
cgit v1.2.3