# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID c47f118fe008ffba936ca97d335e6ee93ca49b99
# Parent  01b8b6fcd857562af8975c9c966ab63904d414f2
renamed "heavy" to "uniform", based on discussion with Nick Smallbone

diff -r 01b8b6fcd857 -r c47f118fe008 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Aug 22 15:02:45 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Aug 22 15:02:45 2011 +0200
@@ -929,7 +929,7 @@
 
 \item[$\bullet$] \textbf{\textit{simple\_higher} (sound):} Exploit simple
 higher-order types if the prover supports the THF syntax; otherwise, fall back
-on \textit{simple} or \textit{mangled\_guards\_heavy}. The problem is
+on \textit{simple} or \textit{mangled\_guards\_uniform}. The problem is
 monomorphized.
 
 \item[$\bullet$]
@@ -960,17 +960,17 @@
 finite (e.g., \textit{bool}). (For \textit{simple} and \textit{simple\_higher},
 the types are not actually erased but rather replaced by a shared uniform type
 of individuals.) As argument to the \textit{metis} proof method, the exclamation
-mark is replaced by a \hbox{``\textit{\_bang}''} suffix.
+mark is replaced by the suffix \hbox{``\textit{\_bang}''}.
 
 \item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
 the ATP and should be the most efficient virtually sound encoding for that ATP.
 \end{enum}
 
 In addition, all the \textit{guards} and \textit{tags} type encodings are
-available in two variants, a lightweight and a heavyweight variant. The
-lightweight variants are generally more efficient and are the default; the
-heavyweight variants are identified by a \textit{\_heavy} suffix (e.g.,
-\textit{mangled\_guards\_heavy}{?}).
+available in two variants, a ``uniform'' and a ``nonuniform'' variant. The
+nonuniform variants are generally more efficient and are the default; the
+uniform variants are identified by the suffix \textit{\_uniform} (e.g.,
+\textit{mangled\_guards\_uniform}{?}).
 
 For SMT solvers, the type encoding is always \textit{simple}, irrespective of
 the value of this option.