aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Integer
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Integer')
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 71d2756011..443777f52a 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -44,8 +44,8 @@ Local Open Scope bigZ_scope.
Notation bigZ := BigZ.t.
Bind Scope bigZ_scope with bigZ BigZ.t BigZ.t_.
-Arguments Scope BigZ.Pos [bigN_scope].
-Arguments Scope BigZ.Neg [bigN_scope].
+Arguments BigZ.Pos _%bigN.
+Arguments BigZ.Neg _%bigN.
Local Notation "0" := BigZ.zero : bigZ_scope.
Local Notation "1" := BigZ.one : bigZ_scope.
Local Notation "2" := BigZ.two : bigZ_scope.