diff options
| author | Cyril Cohen | 2020-06-09 01:16:56 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-09 04:45:15 +0200 |
| commit | 8006cbf40eeb017aacb3ecaa8c4538f9a5aaa3bf (patch) | |
| tree | 805fe2e3ff31c9741ae0ded3cd7ab24b7068f60d /mathcomp/fingroup | |
| parent | 6784363d60493b8ec154bbf1e827ec677d6b5921 (diff) | |
fix coq 8.12 warnings
Diffstat (limited to 'mathcomp/fingroup')
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index b90b35a..c828225 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -170,7 +170,6 @@ Reserved Notation "''N' ( A )" (at level 8, format "''N' ( A )"). Reserved Notation "''N_' G ( A )" (at level 8, G at level 2, format "''N_' G ( A )"). Reserved Notation "A <| B" (at level 70, no associativity). -Reserved Notation "#[ x ]" (at level 0, format "#[ x ]"). Reserved Notation "A <*> B" (at level 40, left associativity). Reserved Notation "[ ~: A1 , A2 , .. , An ]" (at level 0, format "[ ~: '[' A1 , '/' A2 , '/' .. , '/' An ']' ]"). |