Merge pull request #663 from CohenCyril/clean_head

Using Arguments / to deal with volatile definitions

2 files changed, 7 insertions, 8 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 58a3688..31a7aa5 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -508,8 +508,8 @@ Lemma xcfunZr a phi A : xcfun phi (a *: A) = a * xcfun phi A.
 Proof. by rewrite /xcfun linearZ -scalemxAl mxE. Qed.
 
 (* In order to add a second canonical structure on xcfun *)
-Definition xcfun_r_head k A phi := let: tt := k in xcfun phi A.
-Local Notation xcfun_r A := (xcfun_r_head tt A).
+Definition xcfun_r A phi := xcfun phi A.
+Arguments xcfun_r A phi /.
 
 Lemma xcfun_rE A chi : xcfun_r A chi = xcfun chi A. Proof. by []. Qed.
 
@@ -534,7 +534,7 @@ by congr (_ * \tr _) => {A} /=; rewrite /gring_mx /= -rowE rowK mxvecK.
 Qed.
 
 End Char.
-Notation xcfun_r A := (xcfun_r_head tt A).
+Arguments xcfun_r {_ _} A phi /.
 Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope.
 
 Definition pred_Nirr gT B := #|@classes gT B|.-1.
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 2bea267..17b1490 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -378,8 +378,8 @@ Definition cfun_base A : #|classes B ::&: A|.-tuple classfun :=
 Definition classfun_on A := <<cfun_base A>>%VS.
 
 Definition cfdot phi psi := #|B|%:R^-1 * \sum_(x in B) phi x * (psi x)^*.
-Definition cfdotr_head k psi phi := let: tt := k in cfdot phi psi.
-Definition cfnorm_head k phi := let: tt := k in cfdot phi phi.
+Definition cfdotr psi phi := cfdot phi psi.
+Definition cfnorm phi := cfdot phi phi.
 
 Coercion seq_of_cfun phi := [:: phi].
 
@@ -395,7 +395,8 @@ Arguments cfun_indicator {gT} B%g.
 Arguments cfAut {gT B%g} u phi%CF.
 Arguments cfReal {gT B%g} phi%CF.
 Arguments cfdot {gT B%g} phi%CF psi%CF.
-Arguments cfdotr_head {gT B%g} k psi%CF phi%CF.
+Arguments cfdotr {gT B%g} psi%CF phi%CF /.
+Arguments cfnorm {gT B%g} phi%CF /.
 
 Notation "''CF' ( G )" := (classfun G) : type_scope.
 Notation "''CF' ( G )" := (@fullv _ (cfun_vectType G)) : vspace_scope.
@@ -414,8 +415,6 @@ Notation "''[' u , v ]_ G":=  (@cfdot _ G u v) (only parsing) : ring_scope.
 Notation "''[' u , v ]" := (cfdot u v) : ring_scope.
 Notation "''[' u ]_ G" := '[u, u]_G (only parsing) : ring_scope.
 Notation "''[' u ]" := '[u, u] : ring_scope.
-Notation cfdotr := (cfdotr_head tt).
-Notation cfnorm := (cfnorm_head tt).
 
 Section Predicates.