Merge pull request #179 from jashug/deprecate-implicit-arguments

Remove Implicit Arguments command in favor of Arguments

1 files changed, 12 insertions, 12 deletions

diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v
index 995dbee..e0ae1b1 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -641,12 +641,12 @@ Notation "[ 'aspace' 'of' U ]" := (@clone_aspace _ _ U _ _ id)
 Notation "[ 'aspace' 'of' U 'for' A ]" := (@clone_aspace _ _ U A _ idfun)
   (at level 0, format "[ 'aspace'  'of'  U  'for'  A ]") : form_scope.
 
-Implicit Arguments prodvP [K aT U V W].
-Implicit Arguments cent1vP [K aT u v].
-Implicit Arguments centvP [K aT u V].
-Implicit Arguments centvsP [K aT U V].
-Implicit Arguments has_algidP [K aT U].
-Implicit Arguments polyOver1P [K aT p].
+Arguments prodvP [K aT U V W].
+Arguments cent1vP [K aT u v].
+Arguments centvP [K aT u V].
+Arguments centvsP [K aT U V].
+Arguments has_algidP [K aT U].
+Arguments polyOver1P [K aT p].
 
 Section AspaceTheory.
 
@@ -856,8 +856,8 @@ Notation "'C [ u ]" := (centraliser1_aspace u) : aspace_scope.
 Notation "'C ( V )" := (centraliser_aspace V) : aspace_scope.
 Notation "'Z ( A )" := (center_aspace A) : aspace_scope.
 
-Implicit Arguments adim1P [K aT A].
-Implicit Arguments memv_cosetP [K aT U v w].
+Arguments adim1P [K aT A].
+Arguments memv_cosetP [K aT U v w].
 
 Section Closure.
 
@@ -1117,9 +1117,9 @@ Canonical linfun_ahom f := AHom (linfun_is_ahom f).
 
 End Class_Def.
 
-Implicit Arguments ahom_in [aT rT].
-Implicit Arguments ahom_inP [aT rT f U].
-Implicit Arguments ahomP [aT rT f].
+Arguments ahom_in [aT rT].
+Arguments ahom_inP [aT rT f U].
+Arguments ahomP [aT rT f].
 
 Section LRMorphism.
 
@@ -1196,7 +1196,7 @@ Canonical fixedSpace_aspace aT (f : ahom aT aT) := [aspace of fixedSpace f].
 
 End AHom.
 
-Implicit Arguments ahom_in [K aT rT].
+Arguments ahom_in [K aT rT].
 
 Notation "''AHom' ( aT , rT )" := (ahom aT rT) : type_scope.
 Notation "''AEnd' ( aT )" := (ahom aT aT) : type_scope.