Mercurial > cpdt > repo
diff src/DepList.v @ 123:9ccd215e5112
ext_eq
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 18 Oct 2008 17:36:08 -0400 |
parents | 2f97c8177172 |
children | 8a548a6c7074 |
line wrap: on
line diff
--- a/src/DepList.v Sat Oct 18 15:32:59 2008 -0400 +++ b/src/DepList.v Sat Oct 18 17:36:08 2008 -0400 @@ -15,15 +15,15 @@ Section ilist. - Variable A : Set. + Variable A : Type. - Fixpoint ilist (n : nat) : Set := + Fixpoint ilist (n : nat) : Type := match n with | O => unit | S n' => A * ilist n' end%type. - Fixpoint index (n : nat) : Set := + Fixpoint index (n : nat) : Type := match n with | O => Empty_set | S n' => option (index n')