diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index c9cfb7651e5d307b38729b327e6e067458e851b0..56e12f92853514206926b01b7b063eda7fdac06b 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,7 @@
 #   configure	configure
 ###############################################################################
 
+-  E-ACSL       [2018/03/30] Support for let binding.
 -  E-ACSL       [2018/02/21] New option -e-acsl-replace-libc-functions to
 	        replace a few libc functions by built-ins that efficiently
 	        detects when they are incorrectly called.
diff --git a/src/plugins/e-acsl/doc/refman/predicate.tex b/src/plugins/e-acsl/doc/refman/predicate.tex
index a72f293e044dec7a75066461523e44dc2fc9f07b..ae1dcfb610805a2408af395f3996ce3c00116f95 100644
--- a/src/plugins/e-acsl/doc/refman/predicate.tex
+++ b/src/plugins/e-acsl/doc/refman/predicate.tex
@@ -13,7 +13,7 @@
        | [ { pred "^^" pred } ] ; exclusive or
        | [ term "?" pred ":" pred ] ; ternary condition
        | [ pred "?" pred ":" pred ];
-       | { "\let" id "=" term ";" pred }; local binding
+       | "\let" id "=" term ";" pred ; local binding
        | { "\let" id "=" pred ";" pred };
        | [ "\forall" binders ";" ] ; 
            [ integer-guards "==>" pred ]; univ. integer quantification
diff --git a/src/plugins/e-acsl/doc/refman/term.tex b/src/plugins/e-acsl/doc/refman/term.tex
index 33576d7718faf8d054233b5fab1295bf6d704c15..6af096790d609911bff64586e68fff1e7e26180b 100644
--- a/src/plugins/e-acsl/doc/refman/term.tex
+++ b/src/plugins/e-acsl/doc/refman/term.tex
@@ -29,7 +29,7 @@
        | { id "(" term ("," term)* ")" } ; function application
        | "(" term ")" ; parentheses
        | [ term "?" term ":" term ] ; ternary condition
-       | { "\let" id "=" term ";" term } ; local binding
+       | "\let" id "=" term ";" term ; local binding
        | "sizeof" "(" term ")" ;
        | "sizeof" "(" C-type-name ")" ;
        | id ":" term ; syntactic naming