--- a/.hgignore	Wed Oct 16 10:41:23 2013 -0400
+++ b/.hgignore	Thu Dec 05 15:51:33 2013 -0500
@@ -17,6 +17,8 @@
 
 staging/html/.dir
 cpdt.tgz
+cpdtlib.tgz
+cpdtlib
 
 *.glob
 *.v.d

--- a/Makefile	Wed Oct 16 10:41:23 2013 -0400
+++ b/Makefile	Thu Dec 05 15:51:33 2013 -0500
@@ -52,8 +52,16 @@
 cpdt.tgz:
 	hg archive -t tgz $@
 
-install: cpdt.tgz latex/cpdt.pdf latex/exercises.pdf html
-	cp cpdt.tgz staging/
+cpdtlib.tgz: Makefile
+	mkdir -p cpdtlib
+	cp src/LICENSE cpdtlib
+	cp src/CpdtTactics.v cpdtlib
+	cp src/MoreSpecif.v cpdtlib
+	cp src/DepList.v cpdtlib
+	tar zcf cpdtlib.tgz cpdtlib/*
+
+install: cpdt.tgz cpdtlib.tgz latex/cpdt.pdf latex/exercises.pdf html
+	cp cpdt*.tgz staging/
 	cp latex/cpdt.pdf staging/
 	cp latex/exercises.pdf staging/ex/
 	cp -R html staging/

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LICENSE	Thu Dec 05 15:51:33 2013 -0500
@@ -0,0 +1,56 @@
+"Certified Programming with Dependent Types" code license information
+<http://adam.chlipala.net/cpdt/>
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+CAUTION: Most of the source files in this distribution are NOT
+open-source in the usual sense.  See the comment at the beginning of
+each source file for its license, which is Creative Commons, oriented
+more toward free distribution of books than the usual collaborative
+model of open-source software.  The author really is trying to keep
+you from remixing your own versions of the book, which MIT Press might
+not be too happy about.
+
+However, a few of the library modules used here are sufficiently
+useful that they are released separately under a BSD license, included
+below.  The author wants to repeat some advice from the book text,
+though: please don't use these library modules in real projects.  They
+are not designed for any use beside getting the reader up and running
+quickly in reading the book.  All of their content, including the
+"crush" functionality, is rather trivial to implement from scratch for
+your own projects, using the techniques that the book presents.
+
+
+The following license applies ONLY to the source files:
+CpdtTactics.v
+MoreSpecif.v
+DepList.v
+
+~~~~~~~~~~~
+BSD LICENSE
+~~~~~~~~~~~
+
+Copyright (c) 2006-2013, Adam Chlipala
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+- Redistributions of source code must retain the above copyright notice,
+  this list of conditions and the following disclaimer.
+- Redistributions in binary form must reproduce the above copyright notice,
+  this list of conditions and the following disclaimer in the documentation
+  and/or other materials provided with the distribution.
+- The names of contributors may not be used to endorse or promote products
+  derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.

--- a/staging/index.html	Wed Oct 16 10:41:23 2013 -0400
+++ b/staging/index.html	Thu Dec 05 15:51:33 2013 -0500
@@ -23,6 +23,7 @@
 <li> <a href="cpdt.pdf">Latest draft as a PDF</a></li>
 <li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a> [note that the author focuses on the PDF version and doesn't make an effort to keep the HTML version particularly pleasant to use]</li>
 <li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li>
+<li> <a href="cpdtlib.tgz">Tarball of a few generally useful library modules from the book</a> (which are released under an open-source license, while the book generally isn't)</li>
 <li> <a href="repo">Public, read-only Mercurial repository</a></li>
 <li> <a href="updates.rss">RSS feed of updates</a></li>
 </ul>