Change Implicit Arguments to Arguments in odd_order

6 files changed, 31 insertions, 31 deletions

diff --git a/mathcomp/odd_order/BGsection12.v b/mathcomp/odd_order/BGsection12.v
index 7cc32ed..ea39e9d 100644
--- a/mathcomp/odd_order/BGsection12.v
+++ b/mathcomp/odd_order/BGsection12.v
@@ -241,9 +241,9 @@ Qed.
 
 End Introduction.
 
-Implicit Arguments tau2'1 [[M] x].
-Implicit Arguments tau3'1 [[M] x].
-Implicit Arguments tau3'2 [[M] x].
+Arguments tau2'1 {M} [x].
+Arguments tau3'1 {M} [x].
+Arguments tau3'2 {M} [x].
 
 (* This is the rest of B & G, Lemma 12.1 (parts b, c, d,e, and f). *)
 Lemma sigma_compl_context M E E1 E2 E3 :
@@ -2680,7 +2680,7 @@ Qed.
 
 End Section12.
 
-Implicit Arguments tau2'1 [[gT] [M] x].
-Implicit Arguments tau3'1 [[gT] [M] x].
-Implicit Arguments tau3'2 [[gT] [M] x].
+Arguments tau2'1 {gT M} [x].
+Arguments tau3'1 {gT M} [x].
+Arguments tau3'2 {gT M} [x].
 
diff --git a/mathcomp/odd_order/BGsection7.v b/mathcomp/odd_order/BGsection7.v
index 5f803b0..08a589e 100644
--- a/mathcomp/odd_order/BGsection7.v
+++ b/mathcomp/odd_order/BGsection7.v
@@ -267,7 +267,7 @@ Proof. by rewrite inE mmaxJ conjSg !inE. Qed.
 
 Lemma uniq_mmaxP U : reflect (exists M, 'M(U) = [set M]) (U \in 'U).
 Proof. by rewrite inE; apply: cards1P. Qed.
-Implicit Arguments uniq_mmaxP [U].
+Arguments uniq_mmaxP [U].
 
 Lemma mem_uniq_mmax U M : 'M(U) = [set M] -> M \in 'M /\ U \subset M.
 Proof. by move/setP/(_ M); rewrite set11 => /setIdP. Qed.
@@ -354,7 +354,7 @@ Qed.
 
 End MinSimpleOdd.
 
-Implicit Arguments uniq_mmaxP [gT U].
+Arguments uniq_mmaxP [gT U].
 Prenex Implicits uniq_mmaxP.
 
 Notation "''M'" := (minSimple_max_groups _) : group_scope.
diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v
index 6bff279..3c62a9e 100644
--- a/mathcomp/odd_order/PFsection3.v
+++ b/mathcomp/odd_order/PFsection3.v
@@ -260,7 +260,7 @@ suffices ->: sub_bbox (th_bbox th) bb = all in_bb th by apply: allP.
 elim: th => [|[[i j] _] th] //=; case: (th_bbox th) => ri rj /=.
 by rewrite /sub_bbox /= !geq_max andbACA => ->.
 Qed.
-Implicit Arguments th_bboxP [th bb].
+Arguments th_bboxP [th bb].
 
 Fixpoint th_dim th : nat :=
   if th is (_, kvs) :: th1 then
@@ -277,7 +277,7 @@ suffices ->: (th_dim th <= bk)%N = all in_bk th.
 elim: th => // [[_ kvs] th /= <-]; elim: kvs => //= kv kvs.
 by rewrite -andbA geq_max => ->.
 Qed.
-Implicit Arguments th_dimP [th bk].
+Arguments th_dimP [th bk].
 
 (* Theory and clause lookup. *)
 
@@ -468,7 +468,7 @@ split; first by apply/th_bboxP=> cl /thP[].
   by apply/th_dimP=> cl /thP[_ _ clP] kv /clP[].
 by apply/allP=> cl /thP[_ Ucl clP]; rewrite /sat_cl Ucl; apply/allP=> kv /clP[].
 Qed.
-Implicit Arguments satP [m th].
+Arguments satP [m th].
 
 (* Reflexion of the dot product. *)
 
@@ -573,7 +573,7 @@ suffices{Dthx} m_th1: sat m th1.
 apply/satP=> cl1; rewrite Dth1 inE; case: ifP => [_ /eqP-> | _ /thP] //=.
 by rewrite cl'k; split=> // kv /predU1P[-> | /clP//]; rewrite /sat_lit Dv.
 Qed.
-Implicit Arguments sat_cases [m th cl].
+Arguments sat_cases [m th] k [cl].
 
 Definition unsat_cases_hyp th0 kvs tO cl :=
   let: (k, _) := head (2, 0) kvs in let thk_ := ext_cl th0 cl k in
@@ -797,14 +797,14 @@ Proof. by case: find_sym => // s; apply: unsat_match. Qed.
 
 End Interpretation.
 
-Implicit Arguments satP [gT G m th].
-Implicit Arguments unsat [gT G].
-Implicit Arguments sat_cases [gT G m th cl].
-Implicit Arguments unsat_cases [gT G th tO].
-Implicit Arguments unsat_wlog [gT G].
-Implicit Arguments unsat_fill [gT G].
-Implicit Arguments unsat_consider [gT G].
-Implicit Arguments unsat_match [gT G th1 th2].
+Arguments satP [gT G m th].
+Arguments unsat [gT G].
+Arguments sat_cases [gT G m th] k [cl].
+Arguments unsat_cases [gT G th] ij kvs [tO].
+Arguments unsat_wlog [gT G].
+Arguments unsat_fill [gT G].
+Arguments unsat_consider [gT G].
+Arguments unsat_match [gT G] s [th1 th2].
 
 (* The domain-specific tactic language. *)
 
@@ -1829,7 +1829,7 @@ End AutCyclicTI.
 
 End Three.
 
-Implicit Arguments ortho_cycTIiso_vanish [gT G W W1 W2 defW psi].
+Arguments ortho_cycTIiso_vanish [gT G W W1 W2 defW] ctiW [psi].
 
 Section ThreeSymmetry.
 
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.
 
diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v
index e42e104..94e9c42 100644
--- a/mathcomp/odd_order/PFsection5.v
+++ b/mathcomp/odd_order/PFsection5.v
@@ -263,7 +263,7 @@ End Beta.
 
 End SeqInd.
 
-Implicit Arguments seqIndP [calX phi].
+Arguments seqIndP [calX phi].
 
 Lemma seqIndS (calX calY : {set Iirr K}) :
  calX \subset calY -> {subset seqInd calX <= seqInd calY}.
@@ -443,8 +443,8 @@ Proof. by rewrite sum_seqIndD_square ?normal1 ?sub1G // indexg1. Qed.
 
 End InducedIrrs.
 
-Implicit Arguments seqIndP [gT K L calX phi].
-Implicit Arguments seqIndC1P [gT K L phi].
+Arguments seqIndP [gT K L calX phi].
+Arguments seqIndC1P [gT K L phi].
 
 Section Five.
 
@@ -1605,5 +1605,5 @@ End DadeAut.
 
 End Five.
 
-Implicit Arguments coherent_prDade_TIred
-  [gT G H L K W W1 W2 A0 A S0 k tau1 defW].
\ No newline at end of file
+Arguments coherent_prDade_TIred
+  [gT G H L K W W1 W2 S0 A A0 k tau1 defW].
\ No newline at end of file
diff --git a/mathcomp/ssrtest/elim2.v b/mathcomp/ssrtest/elim2.v
index 55c7a81..4ba0b47 100644
--- a/mathcomp/ssrtest/elim2.v
+++ b/mathcomp/ssrtest/elim2.v
@@ -9,7 +9,7 @@ Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F :
   let s := \big[op/idx]_(i <- r | P i) F i in
   K s * K' s -> K' s.
 Proof. by move=> /= [_]. Qed.
-Implicit Arguments big_load [R K' idx op I r P F].
+Arguments big_load [R] K [K' idx op I r P F].
 
 Section Elim1.