Change Implicit Arguments to Arguments in ssreflect

1 files changed, 7 insertions, 7 deletions

diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index 0aafc34..a3e6cac 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -198,7 +198,7 @@ Notation QuotType Q m := (@QuotType_pack _ Q m).
 Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id)
  (at level 0, format "[ 'quotType'  'of'  Q ]") : form_scope.
 
-Implicit Arguments repr [T qT].
+Arguments repr [T qT].
 Prenex Implicits repr.
 
 (************************)
@@ -248,7 +248,7 @@ Notation piE := (@equal_toE _ _).
 Canonical equal_to_pi T (qT : quotType T) (x : T) :=
   @EqualTo _ (\pi_qT x) (\pi x) (erefl _).
 
-Implicit Arguments EqualTo [T x equal_val].
+Arguments EqualTo [T x equal_val].
 Prenex Implicits EqualTo.
 
 Section Morphism.
@@ -276,11 +276,11 @@ Lemma pi_morph11 : \pi (h a) = hq (equal_val x). Proof. by rewrite !piE. Qed.
 
 End Morphism.
 
-Implicit Arguments pi_morph1 [T qT f fq].
-Implicit Arguments pi_morph2 [T qT g gq].
-Implicit Arguments pi_mono1 [T U qT p pq].
-Implicit Arguments pi_mono2 [T U qT r rq].
-Implicit Arguments pi_morph11 [T U qT qU h hq].
+Arguments pi_morph1 [T qT f fq].
+Arguments pi_morph2 [T qT g gq].
+Arguments pi_mono1 [T U qT p pq].
+Arguments pi_mono2 [T U qT r rq].
+Arguments pi_morph11 [T U qT qU h hq].
 Prenex Implicits pi_morph1 pi_morph2 pi_mono1 pi_mono2 pi_morph11.
 
 Notation "{pi_ Q a }" := (equal_to (\pi_Q a)) : quotient_scope.