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/fingroup/perm.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/fingroup/perm.v')
| -rw-r--r-- | mathcomp/fingroup/perm.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 6d9abdc..bbf4363 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -128,7 +128,7 @@ Proof. by move=> x; rewrite -pvalE [@perm]unlock ffunE. Qed. Lemma perm_inj s : injective s. Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed. -Implicit Arguments perm_inj []. +Arguments perm_inj : clear implicits. Hint Resolve perm_inj. Lemma perm_onto s : codom s =i predT. @@ -461,7 +461,7 @@ Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y). Proof. by rewrite -[_ y]mulg1 odd_mul_tperm odd_perm1 addbF. Qed. Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT]. -Implicit Arguments dpair [eT]. +Arguments dpair [eT]. Lemma prod_tpermP s : {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}. @@ -503,7 +503,7 @@ Proof. by rewrite !odd_permM odd_permV addbC addbK. Qed. End PermutationParity. Coercion odd_perm : perm_type >-> bool. -Implicit Arguments dpair [eT]. +Arguments dpair [eT]. Prenex Implicits pcycle dpair pcycles aperm. Section LiftPerm. |