diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 6474f804b2d7876369e55c274f7b676670cd69f1..fdcff5ee23244e7ef1a9f2fc6da98ea781ed7796 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -1382,7 +1382,7 @@ 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
@@ -4131,8 +4131,8 @@ definitions from other 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 the
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,