diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 6d9b6206baeca6c765b323144b0c2956fe614e89..87f624c5635d73241e09d9cd75ae67ae8cdcf7c9 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -5,8 +5,11 @@ release. First we list changes of the last release.
 
 \section*{Frama-C+dev}
 \begin{itemize}
-\item \textbf{Normalizing the Source Code:} document the possibility of
+  \item \textbf{Normalizing the Source Code:} document the possibility of
   undefining builtin macros from the chosen \texttt{-machdep}.
+\item \textbf{Preparing the Sources:} loop pragmas are removed and replaced
+  by dedicated ACSL extension.
+  Use \verb+loop unfold+ in place of \verb+loop pragma UNROLL+.
 \item \textbf{Preparing the Sources:} add subsection on standard library about
   portability considerations.
 \end{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index ed70dadc1916e54a5008ad00443b9d0874832a2b..271b6b6d318b0717e309d747dbcddedaf0df0538 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -304,10 +304,18 @@ underscores as prefix and suffix, \texttt{-UMACRO} will also undefine
   \texttt{do ... while(0)}. This option is set by default.
 
 \item \texttt{\optiondef{-}{ulevel} <n>} unrolls all loops n times. This is a
-  purely syntactic operation.  Loops can be unfolded individually, by
+  purely syntactic operation. Loops can be unfolded individually, by
   inserting a \verb+loop unfold+ annotation just before the loop statement. Do
   not confuse this option with plug-in-specific options that may also be called
-  ``unrolling''~\cite{value}. Below is a typical example of use.
+  ``unrolling''~\cite{value}\footnote{
+    Historically, \textit{syntactic} loop unrolling was denoted by
+    \texttt{loop pragma UNROLL} annotations. Later on, \textsf{EVA} introduced
+    \textit{semantic} unrolling with \texttt{loop unroll} annotations.
+    Loop pragams was removed for Frama-C 29 (Copper) and it was
+    decided to introduce \texttt{loop unfold} annotations for \textit{syntactic}
+    unrolling and to reserve \texttt{loop unroll} annotations for \textit{semantic}
+    loop unrolling with \textsf{EVA}.
+  }. Below is a typical example of use:
 \begin{ccode}
 /*@ loop unfold 10; */
 for(i = 0; i < 9; i++) ...