diff --git a/src/plugins/e-acsl/src/code_generator/translate.mli b/src/plugins/e-acsl/src/code_generator/translate.mli
index f5e814dfaf1bd73ea7ba8de4e57915db290d3bf1..c65e1ab7eebf71ba7a03f8a11c72b8a58667fa45 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate.mli
@@ -53,6 +53,9 @@ val translate_predicate:
     If [pred_to_print] is set, then the runtime check will use this predicate as
     message. *)
 
+val term_to_exp: kernel_function -> Env.t -> term -> exp * Env.t
+(** Convert an ACSL term into a corresponding C expression. *)
+
 val translate_rte_annots:
   (Format.formatter -> 'a -> unit) ->
   'a ->