3 files changed, 7 insertions, 7 deletions
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 62cce1d262..bac50fc457 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.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 86e9eb8ca1..5a2c3cc32b 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -111,7 +111,7 @@ Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z :=
   end.
 
 Definition Zlength := Zlength_aux 0.
-Implicit Arguments Zlength [A].
+Arguments Zlength [A] l.
 
 Section Zlength_properties.
 
@@ -146,6 +146,6 @@ Section Zlength_properties.
 
 End Zlength_properties.
 
-Implicit Arguments Zlength_correct [A].
-Implicit Arguments Zlength_cons [A].
-Implicit Arguments Zlength_nil_inv [A].
+Arguments Zlength_correct [A] l.
+Arguments Zlength_cons [A] x l.
+Arguments Zlength_nil_inv [A] l _.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index e5a92024ff..314f696a21 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -124,7 +124,7 @@ Proof.
   exact (Z_div_mod a b Hb).
 Qed.
 
-Implicit Arguments Zdiv_eucl_exist.
+Arguments Zdiv_eucl_exist : default implicits.
 
 
 (** Uniqueness theorems *)
@@ -679,7 +679,7 @@ Proof.
   rewrite Z.abs_neq; [ assumption | omega ].
 Qed.
 
-Implicit Arguments Zdiv_eucl_extended.
+Arguments Zdiv_eucl_extended : default implicits.
 
 (** * Division and modulo in Z agree with same in nat: *)