Mercurial > cpdt > repo

diff src/Generic.v @ 215:f8bcd33bdd91

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port DataStruct
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 14:00:04 -0500
parents a35eaec19781
children d1464997078d
line wrap: on
line diff
--- a/src/Generic.v	Wed Nov 11 12:21:28 2009 -0500
+++ b/src/Generic.v	Wed Nov 11 14:00:04 2009 -0500
@@ -217,7 +217,7 @@
   Definition datatypeDenoteOk :=
     forall P : T -> Prop,
       (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
-        (forall i : index (recursive c), P (get r i))
+        (forall i : fin (recursive c), P (get r i))
         -> P ((hget dd m) x r))
       -> forall v, P v.