From fe058c3300cf2385f1079fa906cbd13cd2349286 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Thu, 22 Feb 2018 01:57:03 -0800 Subject: Change Implicit Arguments to Arguments in odd_order --- mathcomp/odd_order/PFsection4.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'mathcomp/odd_order/PFsection4.v') 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. -- cgit v1.2.3