diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index ef546063d84e099f17b5c1c8c101bcc4931f2042..a8514fc0dd945aa19088ab45a021b7878c01b97f 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -55,7 +55,6 @@ currently implemented into the \framac's \eacsl plug-in.
       & exclusive or operator \\  %     \lstinline|^^|
       & let bindings \\
       & quantifications over non-integer types \\
-      & \lstinline|\\separated| \\
       & \lstinline|\\specified|
       \\
       \hline
diff --git a/src/plugins/e-acsl/doc/refman/memory.tex b/src/plugins/e-acsl/doc/refman/memory.tex
index 7626c08e864f13b87a275c02a23aac5f06aaef5e..c12a065c89a9bfb264616dd2ec81a83c1de2b4d8 100644
--- a/src/plugins/e-acsl/doc/refman/memory.tex
+++ b/src/plugins/e-acsl/doc/refman/memory.tex
@@ -10,7 +10,7 @@
        | { "\fresh" two-labels? "(" term, term ")" };
        | "\valid" { one-label? } "(" location-address ")" ;
        | "\valid_read" { one-label? } "(" location-address ")";
-       | { "\separated" "(" location-address "," location-addresses ")" };
+       | "\separated" "(" location-address "," location-addresses ")";
        \
   { one-label } ::= { "{" id "}" } ;
        \
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 686b9c95d324a5d4874fc700060a33647aed493d..261843a39061bc86c85aa25af87979fc41abcb77 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -721,8 +721,7 @@ predicates which are related to memory location.
 \subsection{Separation}\label{sec:separation}
 \nodiff
 
-\difficultswhy{\notimplemented{\lstinline|\\separated|}}{the implementation of a
-  memory model}
+\difficultwhy{\lstinline|\\separated|}{the implementation of a memory model}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%