diff options
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 33f50fc9b7..df28b56c8e 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -160,7 +160,7 @@ Qed. Require Import List. -Fixpoint Zlength_aux (acc:Z) (A:Set) (l:list A) {struct l} : Z := +Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) {struct l} : Z := match l with | nil => acc | _ :: l => Zlength_aux (Zsucc acc) A l @@ -171,7 +171,7 @@ Implicit Arguments Zlength [A]. Section Zlength_properties. - Variable A : Set. + Variable A : Type. Implicit Type l : list A. |