diff src/DataStruct.v @ 216:d1464997078d

Switch DepList to inductive, not recursive, types
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 14:28:47 -0500
parents f8bcd33bdd91
children 6601384e7e14
line wrap: on
line diff
--- a/src/DataStruct.v	Wed Nov 11 14:00:04 2009 -0500
+++ b/src/DataStruct.v	Wed Nov 11 14:28:47 2009 -0500
@@ -841,7 +841,7 @@
 
 (** remove printing * *)
 
-(** Some of the type family definitions from this chapter are duplicated in the [DepList] module of the book source.  Only the recursive versions of length-indexed and heterogeneous lists are included, and they are renamed without the [f] prefixes, e.g., [ilist] in place of [filist].
+(** Some of the type family definitions and associated functions from this chapter are duplicated in the [DepList] module of the book source.  Some of their names have been changed to be more sensible in a general context.
 
 %\begin{enumerate}%#<ol>#