From ac6adab9d089d2209aa6aa697b6d75a640adda10 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 11 Dec 2020 19:42:29 +0900
Subject: Change the interpretation scope of some nullary notations from
 ring_scope to fun_scope

---
 mathcomp/algebra/ssrint.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra/ssrint.v')

diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index 9ea0ce4..a51ec47 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -507,7 +507,7 @@ Definition intmul (R : zmodType) (x : R) (n : int) := nosimpl
     | Negz n => (x *- (n.+1))%R
   end.
 
-Notation "*~%R" := (@intmul _) (at level 0, format " *~%R") : ring_scope.
+Notation "*~%R" := (@intmul _) (at level 0, format " *~%R") : fun_scope.
 Notation "x *~ n" := (intmul x n)
   (at level 40, left associativity, format "x  *~  n") : ring_scope.
 Notation intr := ( *~%R 1).
-- 
cgit v1.2.3