Using Arguments / to deal with volatile definitions

4 files changed, 34 insertions, 22 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 77d2e4f..e8c80b1 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 cc3c6c6..921419d 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 e3de209..4ddb8cd 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 455a79e..4a058a6 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.