From 8006cbf40eeb017aacb3ecaa8c4538f9a5aaa3bf Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 9 Jun 2020 01:16:56 +0200
Subject: fix coq 8.12 warnings

---
 mathcomp/fingroup/fingroup.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'mathcomp/fingroup')

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 ']' ]").
-- 
cgit v1.2.3