diff options
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/classfun.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index c8ae7b1..295b77a 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -2488,3 +2488,8 @@ Definition conj_cfQuo := cfAutQuo conjC. Definition conj_cfMod := cfAutMod conjC. Definition conj_cfInd := cfAutInd conjC. Definition cfconjC_eq1 := cfAut_eq1 conjC. + +Notation "@ 'cf_triangle_lerif'" := + (deprecate cf_triangle_lerif cf_triangle_leif) + (at level 10, only parsing). +Notation cf_triangle_lerif := (@cf_triangle_lerif _ _) (only parsing). |