diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-04 18:07:16 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-04 18:07:16 +0000 |
| commit | 43856804207ac43b9ded2609fe7a422db5f62dc4 (patch) | |
| tree | e517f68ce2c43b719f7480ff8f45a0eec0298d46 /theories/ZArith/Zcomplements.v | |
| parent | 58c70113a815a42593c566f64f2de840fc7e48a1 (diff) | |
one more substitution s/Set/Type/
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10617 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
| -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 33f50fc9b..df28b56c8 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. |