aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/character/classfun.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/character/classfun.v')
-rw-r--r--mathcomp/character/classfun.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index a4ecd2c..2048868 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -759,6 +759,7 @@ Arguments classfun_on {gT} B%g A%g.
Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.
Arguments cfun_onP {gT G A phi}.
+Arguments cfConjCK {gT G} phi : rename.
Hint Resolve cfun_onT : core.
Section DotProduct.