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.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 7b2b90d..a4ecd2c 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -759,7 +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}.
-Hint Resolve cfun_onT.
+Hint Resolve cfun_onT : core.
Section DotProduct.