From 7c47bab45686e90ee50e6c7eaae3230cb7ce9e53 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 20 Nov 2020 03:10:59 +0100
Subject: Using Arguments / to deal with volatile definitions

---
 mathcomp/character/character.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/character/character.v')

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index e7ea1e0..c45dc07 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.
-- 
cgit v1.2.3