From cef1a8eadcdef812ce9ee2738cb294644fafbfab Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 21 Feb 2018 23:43:44 -0800
Subject: Change Implicit Arguments to Arguments in solvable

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

(limited to 'mathcomp/solvable/center.v')

diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index 54726be..c461a9e 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -187,7 +187,7 @@ End Injm.
 
 End Center.
 
-Implicit Arguments center_idP [gT A].
+Arguments center_idP [gT A].
 
 Lemma isog_center (aT rT : finGroupType) (G : {group aT}) (H : {group rT}) :
   G \isog H -> 'Z(G) \isog 'Z(H).
-- 
cgit v1.2.3