From 66c7010194f5946cc4f07edc55f92129d0963b99 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Thu, 22 Feb 2018 00:48:18 -0800
Subject: Change Implicit Arguments to Arguments in character

---
 mathcomp/character/vcharacter.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/character/vcharacter.v')

diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 97ad828..5c9ca9b 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -709,7 +709,7 @@ End MoreVchar.
 
 Definition dirr (gT : finGroupType) (B : {set gT}) : pred_class :=  
   [pred f : 'CF(B) | (f \in irr B) || (- f \in irr B)].
-Implicit Arguments dirr [[gT]].
+Arguments dirr {gT}.
 
 Section Norm1vchar.
 
-- 
cgit v1.2.3