diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 894e45b91d8b272fe640c483b299f6c0b512785e..a68b6880da6e645ae0fc22b2fbfc4ee87526fd19 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -105,18 +105,23 @@ end
 (** Imperative environment to perform the fixpoint algorithm for recursive
     functions *)
 module LF_env : sig
-  (* find the currently infered interval for a call to a logic function *)
+  (** find the currently inferred interval for a call to a logic function *)
   val find : logic_info -> Profile.t -> ival
-  (* clear the table of intervals for logic function (to do between typing )
-     each logic function calls *)
+
+  (** clear the table of intervals for logic function (to do between typing )
+      each logic function calls *)
   val clear : unit -> unit
-  (* add an interval for a logic function call *)
+
+  (** add an interval as the current one for a logic function call *)
   val add : logic_info -> Profile.t -> ival -> unit
-  (* add an interval for a predicate call *)
+
+  (** add 0..1 as the current interval for a predicate call *)
   val add_pred : logic_info -> Profile.t -> unit
-  (* determine wether a logic function or predicate is recursive *)
+
+  (** determine whether a logic function or predicate is recursive *)
   val is_rec : logic_info -> bool
-  (* replace the current interval for a logic function call *)
+
+  (** replace the current interval for a logic function call *)
   val replace : logic_info -> Profile.t -> ival -> unit
 end