Merge pull request #663 from CohenCyril/clean_head

Using Arguments / to deal with volatile definitions

7 files changed, 44 insertions, 32 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 9b27ba7..ca71031 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -2429,8 +2429,8 @@ Variables m n p : nat.
 Implicit Type A : 'M[R]_(m, n).
 Implicit Type B : 'M[R]_(n, p).
 
-Definition mulmxr_head t B A := let: tt := t in A *m B.
-Local Notation mulmxr := (mulmxr_head tt).
+Definition mulmxr B A := mulmx A B.
+Arguments mulmxr B A /.
 
 Definition lin_mulmxr B := lin_mx (mulmxr B).
 
@@ -2451,6 +2451,7 @@ Canonical lin_mulmxr_additive := Additive lin_mulmxr_is_linear.
 Canonical lin_mulmxr_linear := Linear lin_mulmxr_is_linear.
 
 End Mulmxr.
+Arguments mulmxr {_ _ _} B A /.
 
 (* The trace. *)
 Section Trace.
@@ -2608,7 +2609,7 @@ Hint Extern 0 (is_true (is_trig_mx (diag_mx _))) =>
 
 Notation "a %:M" := (scalar_mx a) : ring_scope.
 Notation "A *m B" := (mulmx A B) : ring_scope.
-Notation mulmxr := (mulmxr_head tt).
+Arguments mulmxr {_ _ _ _} B A /.
 Notation "\tr A" := (mxtrace A) : ring_scope.
 Notation "'\det' A" := (determinant A) : ring_scope.
 Notation "'\adj' A" := (adjugate A) : ring_scope.
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index dde8843..d707905 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -707,7 +707,7 @@ Qed.
 
 (* A variant of row_free_inj that exposes mulmxr, an alias for mulmx^~ *)
 (* but which is canonically additive *)
-Definition row_free_injr m n p A : row_free A -> injective (@mulmxr A) :=
+Definition row_free_injr m n p A : row_free A -> injective (mulmxr A) :=
   @row_free_inj m n p A.
 
 Lemma row_free_unit n (A : 'M_n) : row_free A = (A \in unitmx).
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index c413171..21e8ada 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -140,7 +140,7 @@ Lemma poly_inj : injective polyseq. Proof. exact: val_inj. Qed.
 Definition poly_of of phant R := polynomial.
 Identity Coercion type_poly_of : poly_of >-> polynomial.
 
-Definition coefp_head h i (p : poly_of (Phant R)) := let: tt := h in p`_i.
+Definition coefp i (p : poly_of (Phant R)) := p`_i.
 
 End Polynomial.
 
@@ -150,9 +150,8 @@ Bind Scope ring_scope with poly_of.
 Bind Scope ring_scope with polynomial.
 Arguments polyseq {R} p%R.
 Arguments poly_inj {R} [p1%R p2%R] : rename.
-Arguments coefp_head {R} h i%N p%R.
+Arguments coefp {R} i%N / p%R.
 Notation "{ 'poly' T }" := (poly_of (Phant T)).
-Notation coefp i := (coefp_head tt i).
 
 Definition poly_countMixin (R : countRingType) :=
   [countMixin of polynomial R by <:].
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index fa952bb..d1f3072 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -1856,22 +1856,22 @@ Include Additive.Exports. (* Allows GRing.additive to resolve conflicts. *)
 Section LiftedZmod.
 Variables (U : Type) (V : zmodType).
 Definition null_fun_head (phV : phant V) of U : V := let: Phant := phV in 0.
-Definition add_fun_head t (f g : U -> V) x := let: tt := t in f x + g x.
-Definition sub_fun_head t (f g : U -> V) x := let: tt := t in f x - g x.
+Definition add_fun (f g : U -> V) x := f x + g x.
+Definition sub_fun (f g : U -> V) x := f x - g x.
 End LiftedZmod.
 
 (* Lifted multiplication. *)
 Section LiftedRing.
 Variables (R : ringType) (T : Type).
 Implicit Type f : T -> R.
-Definition mull_fun_head t a f x := let: tt := t in a * f x.
-Definition mulr_fun_head t a f x := let: tt := t in f x * a.
+Definition mull_fun a f x := a * f x.
+Definition mulr_fun a f x := f x * a.
 End LiftedRing.
 
 (* Lifted linear operations. *)
 Section LiftedScale.
 Variables (R : ringType) (U : Type) (V : lmodType R) (A : lalgType R).
-Definition scale_fun_head t a (f : U -> V) x := let: tt := t in a *: f x.
+Definition scale_fun a (f : U -> V) x := a *: f x.
 Definition in_alg_head (phA : phant A) k : A := let: Phant := phA in k%:A.
 End LiftedScale.
 
@@ -1881,11 +1881,17 @@ Notation null_fun V := (null_fun_head (Phant V)) (only parsing).
 Local Notation in_alg_loc A := (in_alg_head (Phant A)) (only parsing).
 
 Local Notation "\0" := (null_fun _) : ring_scope.
-Local Notation "f \+ g" := (add_fun_head tt f g) : ring_scope.
-Local Notation "f \- g" := (sub_fun_head tt f g) : ring_scope.
-Local Notation "a \*: f" := (scale_fun_head tt a f) : ring_scope.
-Local Notation "x \*o f" := (mull_fun_head tt x f) : ring_scope.
-Local Notation "x \o* f" := (mulr_fun_head tt x f) : ring_scope.
+Local Notation "f \+ g" := (add_fun f g) : ring_scope.
+Local Notation "f \- g" := (sub_fun f g) : ring_scope.
+Local Notation "a \*: f" := (scale_fun a f) : ring_scope.
+Local Notation "x \*o f" := (mull_fun x f) : ring_scope.
+Local Notation "x \o* f" := (mulr_fun x f) : ring_scope.
+
+Arguments add_fun {_ _} f g _ /.
+Arguments sub_fun {_ _} f g _ /.
+Arguments mull_fun {_ _}  a f _ /.
+Arguments mulr_fun {_ _} a f _ /.
+Arguments scale_fun {_ _ _} a f _ /.
 
 Section AdditiveTheory.
 
@@ -6084,11 +6090,17 @@ Notation "*:%R" := (@scale _ _).
 Notation "a *: m" := (scale a m) : ring_scope.
 Notation "k %:A" := (scale k 1) : ring_scope.
 Notation "\0" := (null_fun _) : ring_scope.
-Notation "f \+ g" := (add_fun_head tt f g) : ring_scope.
-Notation "f \- g" := (sub_fun_head tt f g) : ring_scope.
-Notation "a \*: f" := (scale_fun_head tt a f) : ring_scope.
-Notation "x \*o f" := (mull_fun_head tt x f) : ring_scope.
-Notation "x \o* f" := (mulr_fun_head tt x f) : ring_scope.
+Notation "f \+ g" := (add_fun f g) : ring_scope.
+Notation "f \- g" := (sub_fun f g) : ring_scope.
+Notation "a \*: f" := (scale_fun a f) : ring_scope.
+Notation "x \*o f" := (mull_fun x f) : ring_scope.
+Notation "x \o* f" := (mulr_fun x f) : ring_scope.
+
+Arguments add_fun {_ _} f g _ /.
+Arguments sub_fun {_ _} f g _ /.
+Arguments mull_fun {_ _}  a f _ /.
+Arguments mulr_fun {_ _} a f _ /.
+Arguments scale_fun {_ _ _} a f _ /.
 
 Notation "\sum_ ( i <- r | P ) F" :=
   (\big[+%R/0%R]_(i <- r | P%B) F%R) : ring_scope.
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.
 
diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v
index 2fcb8ac..1f8c26f 100644
--- a/mathcomp/solvable/gfunctor.v
+++ b/mathcomp/solvable/gfunctor.v
@@ -148,7 +148,7 @@ Definition monotonic :=
 
 Variables (k : unit) (F1 F2 : object_map).
 
-Definition comp_head : object_map := fun gT A => let: tt := k in F1 (F2 A).
+Definition comp : object_map := fun gT A => F1 (F2 A).
 
 Definition modulo : object_map :=
   fun gT A => coset (F2 A) @*^-1 (F1 (A / (F2 A))).
@@ -244,7 +244,8 @@ Export GFunctor.Exports.
 
 Bind Scope gFun_scope with GFunctor.object_map.
 
-Notation "F1 \o F2" := (GFunctor.comp_head tt F1 F2) : gFun_scope.
+Arguments GFunctor.comp F1 F2 _ /.
+Notation "F1 \o F2" := (GFunctor.comp F1 F2) : gFun_scope.
 Notation "F1 %% F2" := (GFunctor.modulo F1 F2) : gFun_scope.
 
 Section FunctorGroup.