diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf
index 67f2dcbc9aded47915fc062cfa42faeb5d8e618f..fcb304e9554c2055aa14752cf856fd8c396df249 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf differ
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf
index 82d22ecbfa4182a153970d9e5fe668b1b0b7f3bb..0b539ef84e290b5ffab2d23ffaca1f7a7d1392ee 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index f0f8fc90912f6e919674dbfa15d50ec598c50674..7270a3f9554b4680c8a1f5d0ad5397d209403964 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -18,7 +18,7 @@ e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
 
 all: e-acsl
 
-LANGUAGE_VERSION=1.7
+LANGUAGE_VERSION=1.7-1
 EACSL_VERSION= 0.3
 
 EACSL_DIR=$(HOME)/plugins/e-acsl
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index e43f30f93ccbbb2c7faba0712e4b5c8244bccd75..0a33be177e00f7941251fd59f5c2279bd45ab1b1 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -2,6 +2,12 @@
 
 \subsection{Version \version}
 
+\begin{itemize}
+\item \changeinsection{locations}{Fix example \ref{ex:tset}}
+\end{itemize}
+
+\subsection{Version 1.7}
+
 \begin{itemize}
 \item Update according to \acsl 1.7.
 \item \changeinsection{separation}{no more absent}
@@ -80,7 +86,13 @@ in \lstinline|\\at|}
     {
 \section{Changes in \eacsl Implementation}
 
-\subsection{Version \eacslversion}
+\subsection{Version 0.3}
+
+\begin{itemize}
+\item \changeinsection{loop_annot}{support of loop invariant}
+\end{itemize}
+
+\subsection{Version 0.2}
 
 \begin{itemize}
 \item \changeinsection{expressions}{support of bitwise complementation}
diff --git a/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf
index 67f2dcbc9aded47915fc062cfa42faeb5d8e618f..fcb304e9554c2055aa14752cf856fd8c396df249 100644
Binary files a/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf and b/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/e-acsl.pdf b/src/plugins/e-acsl/doc/refman/e-acsl.pdf
index 82d22ecbfa4182a153970d9e5fe668b1b0b7f3bb..0b539ef84e290b5ffab2d23ffaca1f7a7d1392ee 100644
Binary files a/src/plugins/e-acsl/doc/refman/e-acsl.pdf and b/src/plugins/e-acsl/doc/refman/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 9a0c56d7eabea0da2b7f83d72e62b8107e60c082..486e255d88cc2be55ba453aab90828aa19fa7055 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -26,7 +26,7 @@
 \makeindex
 
 \newcommand{\acslversion}{1.7\xspace}
-\newcommand{\version}{\acslversion\xspace}
+\newcommand{\version}{\acslversion-1\xspace}
 
 \renewcommand{\textfraction}{0.01}
 \renewcommand{\topfraction}{0.99}
@@ -85,6 +85,7 @@ Bernard Botella,
 Loīc Correnson,
 Pascal Cuoq,
 Johannes Kanig,
+David Mentr\'e,
 Benjamin Monate,
 Yannick Moy and
 Virgile Prevosto.
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 3d3d6a372a9a7bf9c3e1f2c783ab8fd59c6c413e..3079971445ff6a6a33ac372bf62e5fd991d46ba7 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -368,8 +368,8 @@ members easily identifiable.
 \end{figure}
 
 \begin{notimplementedenv}
-\begin{example}
-The set \lstinlineĩ{ x | integer x; 0 <= x <= 9 && 20 <= x <= 29 }ĩ denotes the
+\begin{example}\label{ex:tset}
+The set \lstinlineĩ{ x | integer x; 0 <= x <= 9 || 20 <= x <= 29 }ĩ denotes the
 set of all integers between 0 and 9 and between 20 and 29.
 \end{example}
 \end{notimplementedenv}