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

Remove Implicit Arguments command in favor of Arguments

1 files changed, 4 insertions, 4 deletions

diff --git a/mathcomp/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v
index b5f9344..2be2adb 100644
--- a/mathcomp/odd_order/PFsection4.v
+++ b/mathcomp/odd_order/PFsection4.v
@@ -692,10 +692,10 @@ Notation primeTIsign ptiW j :=
 Notation primeTIirr ptiW i j := 'chi_(primeTI_Iirr ptiW (i, j)) (only parsing).
 Notation primeTIres ptiW j := 'chi_(primeTI_Ires ptiW j) (only parsing).
 
-Implicit Arguments prTIirr_inj [gT L K W W1 W2 defW x1 x2].
-Implicit Arguments prTIred_inj [gT L K W W1 W2 defW x1 x2].
-Implicit Arguments prTIres_inj [gT L K W W1 W2 defW x1 x2].
-Implicit Arguments not_prTIirr_vanish [gT L K W W1 W2 defW k].
+Arguments prTIirr_inj [gT L K W W1 W2 defW] ptiWL [x1 x2].
+Arguments prTIred_inj [gT L K W W1 W2 defW] ptiWL [x1 x2].
+Arguments prTIres_inj [gT L K W W1 W2 defW] ptiWL [x1 x2].
+Arguments not_prTIirr_vanish [gT L K W W1 W2 defW] ptiWL [k].
 
 Section Four_6_t0_10.