diff --git a/Makefile b/Makefile
index b000a066..822cbede 100644
--- a/Makefile
+++ b/Makefile
@@ -89,7 +89,8 @@ ${PKG}: ${CS_BIN}/cryptol
 	cp examples/DEStest.cry ${PKG}/doc/examples
 	cp examples/Test.cry ${PKG}/doc/examples
 	cp examples/SHA1.cry ${PKG}/doc/examples
-	cp examples/simon.cry ${PKG}/doc/examples
+	cp examples/contrib/simon.cry ${PKG}/doc/examples/contrib
+	cp examples/contrib/spec.cry ${PKG}/doc/examples/contrib
 	cp LICENSE ${PKG}/doc
 
 ${PKG}.tar.gz: ${PKG}
diff --git a/docs/CryptolPrims.markdown b/docs/CryptolPrims.md
similarity index 100%
rename from docs/CryptolPrims.markdown
rename to docs/CryptolPrims.md
diff --git a/docs/Makefile b/docs/Makefile
index 04025134..54c5c47d 100644
--- a/docs/Makefile
+++ b/docs/Makefile
@@ -4,7 +4,7 @@ BOOK = Cryptol.pdf
 .PHONY: all
 all: markdown book
 
-Version2Table.pdf: Version2Table.markdown
+Version2Table.pdf: Version2Table.md
 	pandoc -f markdown+tex_math_dollars $^ -o $@
 
 .PHONY: markdown
@@ -15,7 +15,7 @@ book:
 	(cd ProgrammingCryptol; make)
 	cp ProgrammingCryptol/tmp/${BOOK} .
 
-%.pdf: %.markdown
+%.pdf: %.md
 	pandoc $^ --toc -o $@
 
 .PHONY: clean
diff --git a/docs/ProgrammingCryptol/title/Title.tex b/docs/ProgrammingCryptol/title/Title.tex
index 074874aa..b8df8825 100644
--- a/docs/ProgrammingCryptol/title/Title.tex
+++ b/docs/ProgrammingCryptol/title/Title.tex
@@ -1,6 +1,6 @@
 \noindent
 \begin{center}
-{\LARGE \bf Programming Cryptol}
+{\LARGE \bf Programming in Cryptol}
 
 {\it Levent Erkök\\*
 Dylan McNamee \\*
@@ -18,18 +18,19 @@ Galois, Inc.\\
 Portland, OR 97204
 
 \pagebreak
-\noindent {\bf Acknowledgements}\\
-\vspace{0.5cm} 
-\noindent Cryptol has been under development for over a decade with
-many people contributing to its design and implementation.  Those
-people include Joel Stanley, Joe Hendrix, Aaron Tomb, Adam Wick, Jeff
-Lewis, Philip Weaver, and Sally Browning.
-
-\todo[inline]{2.0: Check with R2D folks about acknowleging Brad Martin,
-  Frank Taylor, and Sean Weaver.}
-
-\todo[inline]{2.0: Do we include Magnus Carlson, Fergus Henderson, Joe
-  Hurd, and John Matthews?}
+\noindent{\bf Acknowledgements}\\
+\\
+\noindent
+Cryptol has been under development for over a decade with many people
+contributing to its design and implementation. Those people include
+Aaron Tomb, Adam Wick, Brian Huffman, Matt Sottile, Adam Foltzer, Joe Hendrix,
+Trevor Elliott,
+David Lazar, Joel Stanley, Jeff Lewis,
+Sigbjørn Finne, Mark Shields, Philip Weaver, Magnus Carlsson, Fergus Henderson, Joe Hurd,
+John Matthews and Sally Browning. In addition, much of the work on Cryptol has been funded by, and
+much design assistance provided by the team at the NSA's Trusted Systems
+Research Group, including (but not limited to) Brad Martin, Frank Taylor and
+Sean Weaver.
 
 \vspace{1in}
 \pagebreak
diff --git a/docs/Syntax.markdown b/docs/Syntax.md
similarity index 100%
rename from docs/Syntax.markdown
rename to docs/Syntax.md
diff --git a/docs/Version2Changes.markdown b/docs/Version2Changes.md
similarity index 100%
rename from docs/Version2Changes.markdown
rename to docs/Version2Changes.md
diff --git a/docs/Version2Table.markdown b/docs/Version2Table.md
similarity index 100%
rename from docs/Version2Table.markdown
rename to docs/Version2Table.md