doc-src/Sledgehammer/sledgehammer.tex

 native higher-order types if the prover supports the THF0 syntax; otherwise,
 falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is
 monomorphized.
 
 \item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native
-polymorphic first-order types if the prover supports the TFF1 syntax; otherwise,
+first-order polymorphic types if the prover supports the TFF1 syntax; otherwise,
 falls back on \textit{mono\_native}.
 
 \item[\labelitemi]
 \textbf{%
 \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\