aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/fingroup
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/fingroup')
-rw-r--r--mathcomp/fingroup/fingroup.v1
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 ']' ]").