diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index a88320e5c920aec6123d2ec2607a26fc3a01b6bc..57512d864ed9c21ed86aff19fc8b4326f320d57a 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -1383,7 +1383,7 @@ warning, but this can be changed by using the
 \paragraph{Source Options.} By default, a message is not localized. You may
 specify a source location, either specifically or by using the current
 location of an \texttt{AST} visitor.
-\lstset{style=frama-c-style}
+\lstset{style=frama-c-style,language=}
 \begin{itemize}
 \item[] \lstinline{~source:$s$} use the source position $s$ (see \texttt{Log.mli})
 \item[] \lstinline{~current:true} use the source location
@@ -4132,8 +4132,8 @@ languages, e.g. \textsf{Coq} or \textsf{Why3}, as regular \acsl module
 definitions. From the user point the view, this takes the form of an extended
 \verb+import+ clause:
 
-\begin{lstlisting}
-//@ import <loader>: <module-name> [ \as <alias-name> ];
+\begin{lstlisting}[style=c]
+//@ import <loader>: <module_name> [ \as <alias-name> ];
 \end{lstlisting}
 
 The syntax is similar to the general ACSL \verb+import+ annotation, except that
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index 8b4212939908fd25efd51404c3016777bc2cbb97..91a947dc0dba4bda4e9c01dda4453dab86a10bcb 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -489,7 +489,7 @@
     \\tainted,
     Here,LoopCurrent,LoopEntry,Pre,Post,Old,
     \\Cons,\\Down,\\NearestAway,\\NearestEven,\\Nil,\\ToZero,\\Up,
-    \\at,\\allocable,\\allocation,\\automatic,\\base_addr,\\block_length,\\dangling,
+    \\as,\\at,\\allocable,\\allocation,\\automatic,\\base_addr,\\block_length,\\dangling,
     \\dynamic,\\exists,\\exit_status,\\false,\\forall,\\freeable,\\fresh,\\from,
     \\in,\\initialized,\\lambda,\\let,\\list,\\match,\\nothing,\\null,\\numof,
     \\object_pointer,\\offset,\\old,\\register,\\result,\\separated,\\static,