# HG changeset patch
# User blanchet
# Date 1301993256 -7200
# Node ID 7ec43598c8bed38eece1c07eb8ba247dc226280d
# Parent  aab49f3cf80224634c931619cfd1d038eec22be0
minor doc edits

diff -r aab49f3cf802 -r 7ec43598c8be doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Apr 05 10:37:21 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Apr 05 10:47:36 2011 +0200
@@ -564,19 +564,16 @@
 \item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
 its type.
 
-% NOT YET IMPLEMENTED:
-%\item[$\bullet$] \textbf{\textit{preds}:} Types are represented by predicates.
-
 \item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names.
 This value is available only if \textit{monomorphize} is enabled and
-\textit{full\_types} is enabled.
+\textit{full\_types} is disabled.
 
 \item[$\bullet$] \textbf{\textit{const\_args}:} Constants are annotated with
-their type parameters, which are passed as extra arguments. This value is not
-available if \textit{full\_types} is enabled.
+their type parameters, which are passed as extra arguments. This value is
+ignored if \textit{full\_types} is enabled.
 
 \item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
-ATP.
+ATP. This value is ignored if \textit{full\_types} is enabled.
 
 \item[$\bullet$] \textbf{\textit{smart}:} This is the same as
 \textit{tags} if \textit{full\_types} is enabled; otherwise, this is the