diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 4403388e929e6f3fa1e68f2eb5ca3654e4204c03..53e00589c68918868f6b7b5ae278574979131ebf 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -1,5 +1,20 @@
 \chapter{ACSL extensions} % here we do not use the macro (avoids a warning)
 \label{cha:acsl-extensions}
+\section{Extension syntaxes}
+\label{acsl:syntax}
+
+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 _|.
+
+The complete syntax is usefull 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. 
+
 \section{Handling indirect calls with \texttt{calls}}
 \label{acsl:calls}
 
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index e218020b3eeff9a0864db565efb08e7e9f6941fb..e2a8eae1f2c2b9182c7c0eadd466dad0e2518fd0 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -321,7 +321,7 @@
           "Unregistered extension %s for plug-in %s" s plugin
       else
         Kernel.warning ~once:true ~wkey:Kernel.wkey_plugin_not_loaded ~source
-          "Ignored extensions for unregistered plug-in %s" plugin;
+          "Ignored extensions for unloaded plug-in %s" plugin;
       IDENTIFIER_EXT s
     | EXT_CODE_ANNOT s
     | EXT_GLOBAL s
@@ -594,8 +594,7 @@ and comment = parse
       | Logic_utils.Not_well_formed (loc, m) ->
         output ~source:(fst loc) "%s" m;
         None
-      | Logic_utils.Unknown_ext ->
-        None
+      | Logic_utils.Unknown_ext -> None
       | Log.FeatureRequest(source,_,msg) ->
         let source = Option.value ~default:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) source in
         output ~source "unimplemented ACSL feature: %s" msg; None
diff --git a/tests/spec/oracle/Extend_warning.res.oracle b/tests/spec/oracle/Extend_warning.res.oracle
index 47dbc6e2c8def833ac79f32d6234238c88b258e0..e897425bd86a1d476c6219130006d1103378cd11 100644
--- a/tests/spec/oracle/Extend_warning.res.oracle
+++ b/tests/spec/oracle/Extend_warning.res.oracle
@@ -4,7 +4,7 @@
 [kernel:extension-unknown] Extend_warning.i:7: Warning: 
   Unregistered extension bar for plug-in myplugin
 [kernel:plugin-not-loaded] Extend_warning.i:8: Warning: 
-  Ignored extensions for unregistered plug-in unknown_plugin
+  Ignored extensions for unloaded plug-in unknown_plugin
 /* Generated by Frama-C */
 /*@ \myplugin::foo x ≡ 0; */
 int f(int x)