diff --git a/doc/rte/rte.tex b/doc/rte/rte.tex
index 65daa15731ba18fe797a88d14ba3bbfcea4e86b6..bea711914f6c2cca3817d6014b0fe707df778ee5 100644
--- a/doc/rte/rte.tex
+++ b/doc/rte/rte.tex
@@ -875,8 +875,7 @@ left-values access \\
 \lstinline |-rte-float-to-int| & boolean (true) & Generate annotations for
 casts from floating-point to integer \\
 \hline
-\lstinline |-rte-trivial-annotations| & boolean (true) & Generate status for
-annotation through constant folding \\
+\lstinline |-rte-trivial-annotations| & boolean (true) & Generate all annotations even when they trivially hold \\
 \hline
 \lstinline |-rte-warn| & boolean (true) & Emit warning on broken annotations \\
 \hline
diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml
index 0b629f7f9941d8f09e6494f4e3c8ca20611539c1..5d7801695966c21eddbaee91d44e0038a33ea650 100644
--- a/src/plugins/rte/options.ml
+++ b/src/plugins/rte/options.ml
@@ -90,14 +90,16 @@ module DoPointerCall =
     end)
 
 (* uses results of basic constant propagation in order to check
-   validity / invalidity of generated assertions, emitting a status if possible
+   validity / invalidity of generated assertions, emitting a status if possible.
+   Notice that annotations that can be considered valid from syntaxical rules
+   are also considered as trivial.
 *)
 module Trivial =
   False
     (struct
       let option_name = "-rte-trivial-annotations"
-      let help = "generate annotations for constant expressions, even when \
-                  they trivially hold"
+      let help = "generate all annotations even when they trivially hold \
+                  (from evaluation of constant expressions, syntactical rules...)"
       (* if on, evaluates constants in order to check if assertions
          are trivially true / false *)
     end)