[eacsl:doc] Update reference and implementation manual

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

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 "}" } ;
        \

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}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%