diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 10c1a2f55dc671aa6c3c61bf3852a10c8d7c0971..5431caaf077f8d66a641773f0c058cf2a5fdd365 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -839,14 +839,6 @@ The available \textsf{WP} command-line options related to model selection are:
   in \textsf{ACSL} contracts to ensure type-checking but are related to identity-casts
   from the code. The option is \texttt{off} by default.
 
-\item[\tt -wp-bool-range] experimental support for \verb+_Bool+ range. This option assumes
-  there is no \emph{trap representations}
-  in considering valid the related assertions generated by \texttt{-wp-rte} (those tagged with \texttt{bool\_value:}).
-  Hence, integer values with boolean type are
-  either equal to \verb+0+ or \verb+1+. Actually, the only way to forge other values
-  is \emph{via} union types and heterogeneous pointer casts, which is currently not allowed
-  in the memory models of \textsf{WP}.
-
 \item[\tt -wp-literals] exports the contents of string literals
   to provers (default: \texttt{no}).
 \item[\tt -wp-extern-arrays] gives an arbitrary large size to arrays
@@ -861,6 +853,7 @@ The available \textsf{WP} command-line options related to model selection are:
       \texttt{ref}: & the variable is a constant pointer and is modeled by the \texttt{Ref}.\\
       \texttt{context}: & the variable is initially non-aliased and uses a fresh global in \texttt{Typed}.\\
   \end{tabular}
+\item[\tt -wp-(no)-alias-init] Use initializers for aliasing propagation (default is: yes).
 \item[\tt -wp-(no)-volatile] this option (de)activate the correct handling of
   volatile access. By default, accessing a volatile l-value returns an undefined
   value, and writing to a volatile l-value is modeled like an \textsf{ACSL} assigns clause.
@@ -1029,7 +1022,7 @@ Support for \textsf{Why-3 IDE} is no longer provided.
   Default is \verb+5s+.
 \item[\tt -wp-steps <$n$>] sets the maximal number of prover
   steps. This can be used as a machine-independent alternative to timeout.
-\item[\tt -wp-why-opt='options,...'] provides additional options to the
+\item[\tt -wp-why3-opt='options,...'] provides additional options to the
   \verb+why3+ command.
 \item[\tt -wp-why3='<cmd>'] overrides the path to the \verb+why3+ command.
 \end{description}
@@ -1102,27 +1095,6 @@ procedures.  This support is provided for \textsf{Alt-Ergo},
 \item[\tt -wp-share <dir>] modifies the default directory where
   resources are found.  This option can be useful for running a modified or
   patched distribution of \textsf{WP}.
-% \item[\tt -wp-include <dir,\ldots,++sharedir>] (\textbf{deprecated} use driver instead) sets the directories where external
-%   libraries and driver files are looked for.
-%   The current directory (implicitly added to that list) is always looked up
-%   first.
-%   Relative directory names are relative to the current directory except
-%   for names prefixed by the characters \texttt{++}.
-%   In such a name, the directory is relative to the main \texttt{FRAMAC\_SHARE}
-%   directory.
-% \item[\tt -wp-alt-ergo-lib <f,\ldots>] (\textbf{deprecated} use altergo.file
-%   in driver instead) looks for \textsf{Alt-Ergo}
-%   library files \verb+"f.mlw"+ and inlines them into the proof
-%   obligation files for \textsf{Alt-Ergo}.
-% \item[\tt -wp-coq-lib <f,\ldots>] (\textbf{deprecated} use coq.file
-%   in driver instead) looks for \textsf{Coq} files
-%   \verb+"f.v"+ or \verb+"f.vo"+. If
-%   \verb+"f.vo"+ is not found, then \textsf{WP} copies \verb+"f.v"+
-%   into its working directory (see option
-%   \texttt{-wp-out}) and compiles it locally.
-% \item[\tt -wp-why-lib <f,\ldots>] (\textbf{deprecated} use why3.file in driver instead) looks for \textsf{Why3} library file
-%   \verb+"f.why"+ and opens the library \verb+"f.F"+ for the proving the
-%   goals.
 \end{description}
 
 \subsection{Linking \textsf{ACSL} Symbols to External Libraries}
@@ -1136,8 +1108,7 @@ if any, are not exported by \textsf{WP}s.
 External linkage is specified in \emph{driver files}. It is possible
 to load one or several drivers with the following \textsf{WP} plug-in option:
 \begin{description}
-\item[\tt -wp-driver <file,\ldots>] load specified driver files,
-  replacing deprecated features from section~\ref{prooflibs}.
+\item[\tt -wp-driver <file,\ldots>] load specified driver files.
 
 \end{description}
 
@@ -1280,11 +1251,8 @@ interactively or incrementally, it is often the case where most proof obligation
 from one \textsf{WP} execution to the other. To reduce this costs, a cache of prover results can be used
 and stored in your session.
 
-The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo}
-and \textsf{Coq} provers -- although proof scripts works with both.
-There are different ways of using the cache, depending on your precise needs.
-
-The \textsf{WP} options to control session and cache are \verb+-wp-session+ and \verb+-wp-cache+, as documented below:
+The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo} and \textsf{Coq} provers. There are different ways of using the cache, depending on your precise needs.
+The main option to control cache usage is \verb+-wp-cache+, documented below:
 
 \begin{description}
 \item[\tt -wp-session <dir>] select the directory where cached results and proof scripts