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/commutator.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v
index 1f9bad0..6a390ce 100644
--- a/mathcomp/solvable/commutator.v
+++ b/mathcomp/solvable/commutator.v
@@ -352,7 +352,7 @@ Proof. exact: commG1P. Qed.
 
 End Commutator_properties.
 
-Implicit Arguments derG1P [gT G].
+Arguments derG1P [gT G].
 
 Lemma der_cont n : GFunctor.continuous (derived_at n).
 Proof. by move=> aT rT G f; rewrite morphim_der. Qed.
-- 
cgit v1.2.3