diff options
| author | Kazuhiko Sakaguchi | 2019-05-21 17:36:39 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-12-11 14:26:52 +0100 |
| commit | ebd828b4939f105d7ea7d7bb950b5dcfd6887981 (patch) | |
| tree | 1fce21fdadf105e971d5ba36159fd775e000d137 /mathcomp/character | |
| parent | 6d34f29cf906b6672925ee3abd4e54b59eea784f (diff) | |
Use `deprecate` notation in ssrnum
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). |