diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 3b4015a6d13aec305165d9324c7333ca25426afb..27d9be4791f802dbe9eebcb8cd3ed69c8cbe2139 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -61,9 +61,9 @@
 
 @inproceedings{rvcubes17tool,
   author = {Julien Signoles and Nikolai Kosmatov and Kostyantyn Vorobyov},
-  title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C 
+  title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C
 Programs. Tool Paper}},
-  booktitle = {International Workshop on Competitions, Usability, Benchmarks, 
+  booktitle = {International Workshop on Competitions, Usability, Benchmarks,
 Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES)},
   year = 2017,
   month = sep,
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index c03e86a05a1530466d98980026b7a4d8fd0f66f0..7ba7552f5345c4a6a137cc15874a534b7da573db 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -13,12 +13,12 @@ release. First we list changes of the last release.
 
 \begin{itemize}
 \item \textbf{Introduction}: Improve a bit and reference related papers.
-\item \textbf{Wat the Plug-in Provides}: Highlight that the memory analysis is
+\item \textbf{What the Plug-in Provides}: Highlight that the memory analysis is
   not yet robust.
-\item \textbf{Wat the Plug-in Provides}: Highlight the importance of
+\item \textbf{What the Plug-in Provides}: Highlight the importance of
   \textbf{-e-acsl-prepare}.
-\item \textbf{Known Limitations}: Add the section ``Supported Systems'' that
-  replaces the former section ``Limitations of E-ACSL Monitoring Libraries''.
+\item \textbf{Known Limitations}: Replace section ``Limitations of E-ACSL
+  Monitoring Libraries'' by the new section ``Supported Systems''.
 \end{itemize}
 
 \section*{E-ACSL Chlorine-20180501}
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index 0a8919021500437be2bc16af9e691258424efe4a..1f263c145d11bfd25907b8fb67e7b1b62498321e 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -14,7 +14,8 @@ program.
 \C code and perform what is usually referred to as ``runtime assertion
 checking''~\cite{runtime-assertion-checking}\footnote{In our context, ``runtime
   annotation checking'' would be more precise.}. This is the primary goal of
-\eacsl. Indirectly, in combination with plug-in \rte~\cite{rte} of \framac, this
+\eacsl. Indirectly, in combination with the \rte plug-in~\cite{rte} of \framac,
+this 
 usage allows the user to detect undefined behaviors in its \C code. Second, it
 allows to combine \framac and its existing analyzers with other \C analyzers
 that do not natively understand the \acsl specification language. Third, the
@@ -23,7 +24,7 @@ very helpful while writing a correct specification of a given program,
 \emph{e.g.} for later program proving.  Finally, an executable specification
 makes it possible to check assertions that cannot be verified statically and
 thus to establish a link between runtime monitoring and static analysis tools
-such as \Eva~\cite{eva}\index{Eva} or \wpplugin~\cite{wp}\index{Wp}. 
+such as \Eva~\cite{eva}\index{Eva} or \wpplugin~\cite{wp}\index{Wp}.
 
 Annotations used by the plug-in must be written in the \eacsl specification
 language~\cite{eacsl,sac13} -- a subset of \acsl. \eacsl plug-in is still in a
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 2ef04f8110827e04e46252d1c15a43d2c1efa78e..24a3aced3bac7aac92df0a1a8064b8dd5ac123dc 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -20,7 +20,7 @@ The only well-supported system is a Linux distribution on a 64-bit architecture.
 
 \subsection{Operating Systems}
 
-Not-Linux systems are almost not yet experimented. It might work but there are
+Non-Linux systems are almost not yet experimented. It might work but there are
 most probably issues, in particular if using a non-standard
 libc\index{Libc}. For instance, there are known bugs under Mac OS
 X\index{Mac OS X}\footnote{See for instance at