aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Int.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Int.v')
-rw-r--r--theories/ZArith/Int.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 62cce1d26..bac50fc45 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -27,7 +27,7 @@ Module Type Int.
Parameter int : Set.
Parameter i2z : int -> Z.
- Arguments Scope i2z [ Int_scope ].
+ Arguments i2z _%I.
Parameter _0 : int.
Parameter _1 : int.