diff options
| author | Anton Trunov | 2018-11-20 17:51:11 +0100 |
|---|---|---|
| committer | Anton Trunov | 2018-11-21 16:23:02 +0100 |
| commit | f049e51c39077a025907ea87c08178dad1841801 (patch) | |
| tree | 2ffb41f5afa11a147989c8efcc1dcb295ae2ed2b /mathcomp/character/classfun.v | |
| parent | 967088a6f87405a93ce21971392c58996df8c99f (diff) | |
Merge Arguments and Prenex Implicits
See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
Diffstat (limited to 'mathcomp/character/classfun.v')
| -rw-r--r-- | mathcomp/character/classfun.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 7a0e538..ac3e5bc 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -557,7 +557,7 @@ rewrite big1 ?addr0 // => _ /andP[/imsetP[y Gy ->]]; apply: contraNeq. rewrite cfunE cfun_repr cfun_classE Gy mulf_eq0 => /norP[_]. by rewrite pnatr_eq0 -lt0n lt0b => /class_eqP->. Qed. -Arguments cfun_onP [A phi]. +Arguments cfun_onP {A phi}. Lemma cfun_on0 A phi x : phi \in 'CF(G, A) -> x \notin A -> phi x = 0. Proof. by move/cfun_onP; apply. Qed. @@ -759,7 +759,7 @@ End ClassFun. Arguments classfun_on _ _%g _%g. Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope. -Arguments cfun_onP [gT G A phi]. +Arguments cfun_onP {gT G A phi}. Hint Resolve cfun_onT. Section DotProduct. @@ -1009,7 +1009,7 @@ Lemma orthoPl phi S : Proof. by rewrite [orthogonal _ S]andbT /=; apply: (iffP allP) => ophiS ? /ophiS/eqP. Qed. -Arguments orthoPl [phi S]. +Arguments orthoPl {phi S}. Lemma orthogonal_sym : symmetric (@orthogonal _ G). Proof. @@ -1242,12 +1242,12 @@ Qed. End DotProduct. -Arguments orthoP [gT G phi psi]. -Arguments orthoPl [gT G phi S]. -Arguments orthoPr [gT G S psi]. -Arguments orthogonalP [gT G S R]. -Arguments pairwise_orthogonalP [gT G S]. -Arguments orthonormalP [gT G S]. +Arguments orthoP {gT G phi psi}. +Arguments orthoPl {gT G phi S}. +Arguments orthoPr {gT G S psi}. +Arguments orthogonalP {gT G S R}. +Arguments pairwise_orthogonalP {gT G S}. +Arguments orthonormalP {gT G S}. Section CfunOrder. @@ -1273,7 +1273,7 @@ Proof. by apply/eqP; rewrite -dvdn_cforder. Qed. End CfunOrder. -Arguments dvdn_cforderP [gT G phi n]. +Arguments dvdn_cforderP {gT G phi n}. Section MorphOrder. |