--- a/src/DepList.v	Wed Nov 11 12:21:28 2009 -0500
+++ b/src/DepList.v	Wed Nov 11 14:00:04 2009 -0500
@@ -31,14 +31,14 @@
 
   Implicit Arguments icons [n].
 
-  Fixpoint index (n : nat) : Type :=
+  Fixpoint fin (n : nat) : Type :=
     match n with
       | O => Empty_set
-      | S n' => option (index n')
+      | S n' => option (fin n')
     end.
 
-  Fixpoint get (n : nat) : ilist n -> index n -> A :=
-    match n return ilist n -> index n -> A with
+  Fixpoint get (n : nat) : ilist n -> fin n -> A :=
+    match n return ilist n -> fin n -> A with
       | O => fun _ idx => match idx with end
       | S n' => fun ls idx =>
         match idx with