diff --git a/docs/ProgrammingCryptol.pdf b/docs/ProgrammingCryptol.pdf
index 9d336d09..ea4356d3 100644
Binary files a/docs/ProgrammingCryptol.pdf and b/docs/ProgrammingCryptol.pdf differ
diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
index 88eed487..ff6c4c91 100644
--- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
+++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
@@ -3445,7 +3445,7 @@ equivalent:
 Sometimes it it useful to be able to define a truly \emph{new} type
 that the typechecker will recognize as distinct from all other types.
 For example, one might wish to define a type with internal invariants,
-or use a collection of data in a way is semantically different from
+or use a collection of data in a way that is semantically different from
 the default implementations of arithmetic or comparison.  For
 situations like this, where the programmer desires a lightweight
 abstraction barrier, a \texttt{newtype} declaration allows the