diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 53e00589c68918868f6b7b5ae278574979131ebf..9da27d2c8d42b8632a4a59898c58a93c5ba374e1 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -6,14 +6,15 @@
 When a plug-in registers an extension, it can be used in \acsl annotations
 with 2 different syntaxes. As an example, with an extension \lstinline|bar|
 registered by the plug-in \lstinline|foo|, we can use the short syntax
-\lstinline|bar _| and the complete syntax \lstinline|\foo::bar _|.
+\lstinline|bar _| or the complete syntax \lstinline|\foo::bar _|.
 
-The complete syntax is usefull to print better warning/error messages, and to
+The complete syntax is useful to print better warning/error messages, and to
 better understand which plug-in introduced the extension. Additionnaly, all
 extensions coming from an unloaded plug-in can be ignored this way. For
 example, if \Eva is not loaded, \lstinline|\eva::unroll _| annotations will be
-ignored with a warning, unlike \lstinline|unroll _| which by default will be
-treated as a user error. 
+ignored with a warning, whereas \lstinline|unroll _| cannot be identified as
+being supported by Eva, which means that it can only be treated as a user
+error. 
 
 \section{Handling indirect calls with \texttt{calls}}
 \label{acsl:calls}
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index 748849d1d76051bcac12cef42dede6bf5b3e8ff8..16d93d84415489f0aa68f7e1633708842a5b77e0 100644
--- a/tests/libc/stdlib_c.c
+++ b/tests/libc/stdlib_c.c
@@ -2,7 +2,7 @@
    STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-msg-key malloc"
    STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
    STDOPT: #"-eva-no-builtins-auto"
-*/ // \eva::slevel is used to \eva::unroll loops
+*/ // \eva::slevel is used to unroll loops
 
 #define malloc(n) Frama_C_malloc(n)
 #include "stdlib.c"
diff --git a/tests/libc/string_c.c b/tests/libc/string_c.c
index eeb65f0a999d665bfa1f0619ffa0933ec4593658..3fb1d5a8056383639fbbbb61bcb5777f06f8393d 100644
--- a/tests/libc/string_c.c
+++ b/tests/libc/string_c.c
@@ -1,6 +1,6 @@
 /* run.config
    STDOPT: #"-eva-no-builtins-auto -eva-slevel 1000 -eva-no-skip-stdlib-specs"
-*/ // \eva::slevel is used to \eva::unroll loops
+*/ // \eva::slevel is used to unroll loops
 
 #include "string.c"
 volatile int v;