diff options
| author | Enrico | 2018-03-03 10:30:33 +0100 |
|---|---|---|
| committer | GitHub | 2018-03-03 10:30:33 +0100 |
| commit | 6f075b64b936de9ee4fa79ea4dc1d2fb9b9cf2c8 (patch) | |
| tree | 59cc350ed0be586e871e56e41b48939b08032929 /mathcomp/odd_order/PFsection5.v | |
| parent | 22692863c2b51cb6b3220e9601d7c237b1830f18 (diff) | |
| parent | fe058c3300cf2385f1079fa906cbd13cd2349286 (diff) | |
Merge pull request #179 from jashug/deprecate-implicit-arguments
Remove Implicit Arguments command in favor of Arguments
Diffstat (limited to 'mathcomp/odd_order/PFsection5.v')
| -rw-r--r-- | mathcomp/odd_order/PFsection5.v | 10 |
1 files changed, 5 insertions, 5 deletions
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 |