Merge pull request #663 from CohenCyril/clean_head

Using Arguments / to deal with volatile definitions

1 files changed, 4 insertions, 3 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.