diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst
index 906f3614..bcebebf0 100644
--- a/cryptol-remote-api/docs/Cryptol.rst
+++ b/cryptol-remote-api/docs/Cryptol.rst
@@ -23,7 +23,7 @@ zero or more of the following fields:
    + ``base``: What base to display numbers in (default ``10``).
    + ``prefix of infinite lengths``: How much of an infinite sequence to display (default ``5``.
    + ``floating point base``: What base to display floating point numbers in (default ``10``).
-   + ``floating point format``: The output format used to display floating point numbers (accepts strings in the same format as the argument to ``:set fp-format`` in the REPL).
+   + ``floating point format``: The output format used to display floating point numbers (accepts strings in the same format as the argument to ``:set fpFormat`` in the REPL).
 
 Module Management
 =================
diff --git a/docs/ProgrammingCryptol.pdf b/docs/ProgrammingCryptol.pdf
index 7d4c6cc9..9d336d09 100644
Binary files a/docs/ProgrammingCryptol.pdf and b/docs/ProgrammingCryptol.pdf differ
diff --git a/docs/ProgrammingCryptol/technicalities/TechAppendix.tex b/docs/ProgrammingCryptol/technicalities/TechAppendix.tex
index 1004f85f..08f829dc 100644
--- a/docs/ProgrammingCryptol/technicalities/TechAppendix.tex
+++ b/docs/ProgrammingCryptol/technicalities/TechAppendix.tex
@@ -160,12 +160,12 @@ have defined, along with their types.
     \hline
      \texttt{ascii}           & \texttt{off}   & print sequences of bytes as a string \\
      \texttt{base}            & \texttt{16}    & numeric base for printing words  \\
-     \texttt{ignore-safety}   & \texttt{off}   & ignore safety predicates when performing \texttt{:sat} or \texttt{:prove} checks \\
+     \texttt{ignoreSafety}   & \texttt{off}   & ignore safety predicates when performing \texttt{:sat} or \texttt{:prove} checks \\
      \texttt{infLength}       & \texttt{5}     & number of elements to show from an infinite sequence \\
      \texttt{prover}          & \texttt{z3}    & which SMT solver to use for \texttt{:prove}  \\
      \texttt{satNum}          & \texttt{1}     & maximum number of solutions to show for \texttt{:sat} \\
-     \texttt{show-examples}   & \texttt{on}    & whether to print counterexamples and models \\
-     \texttt{smtfile}         & \texttt{-}     & file to write SMT problems when \texttt{prover = offline} \\
+     \texttt{showExamples}   & \texttt{on}    & whether to print counterexamples and models \\
+     \texttt{smtFile}         & \texttt{-}     & file to write SMT problems when \texttt{prover = offline} \\
      \texttt{tests}           & \texttt{100}   & number of tests to run for \texttt{:check} \\
     \hline
   \end{tabular*}