diff --git a/src/plugins/e-acsl/functions.mli b/src/plugins/e-acsl/functions.mli
index 4c1c01fefdaa5b47c9ec3b0ef6a2e7b49353fbf7..c549f3abc4c59ac67bc7eb7a1dc4351ee54b74e3 100644
--- a/src/plugins/e-acsl/functions.mli
+++ b/src/plugins/e-acsl/functions.mli
@@ -61,7 +61,7 @@ module RTL: sig
 
   val is_rtl_name: string -> bool
   (** @return [true] if the prefix of the given name indicates that it
-      belongs to the public API of the E-ACSL Runtime Realary *)
+      belongs to the public API of the E-ACSL Runtime Library *)
 
   val is_generated_literal_string_name: string -> bool
   (** Same as [is_generated_name] but indicates that the name represents a local
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index e041ef8e7d32ca005cd63b9c42332b54e82085de..bd97b36428944ea8ef8877154fbe5468dd48d83f 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -63,7 +63,8 @@ val interv_of_typ: Cil_types.typ -> Ival.t
 (** @return the smallest interval which contains the given C type.
     @raise Is_a_real if the given type is a float type.
       (* TODO: also return is_real=true if ty=Real.t *)
-    @raise Not_a_number if the given type does not represent numbers. *)
+    (* TODO RATIONAL: why not returning [-\infty; +\infty]? *)
+    @raise Not_a_number if the given type does not represent any number. *)
 
 (* ************************************************************************** *)
 (** {3 Environment for interval computations} *)
@@ -85,8 +86,10 @@ end
 val infer: Cil_types.term -> Ival.t
 (** [infer t] infers the smallest possible integer interval which the values
     of the term can fit in.
-    @raise Is_a_real if the term is a float or a real
-    @raise Not_a_number if the term does not represent a number. *)
+    @raise Is_a_real if the term is either a float or a real.
+(*  TODO RATIONAL: why raising Is_a_real since Eva is able to infer such *)
+    intervals?
+    @raise Not_a_number if the term does not represent any number. *)
 
 (*
 Local Variables:
diff --git a/src/plugins/e-acsl/temporal.ml b/src/plugins/e-acsl/temporal.ml
index e7bf4e973761b80fdabd9f309cc9f8761ef36771..d624f2ebd5759775f0ffba685a311267ac90a572 100644
--- a/src/plugins/e-acsl/temporal.ml
+++ b/src/plugins/e-acsl/temporal.ml
@@ -284,7 +284,7 @@ end = struct
     let rhs = Cil.new_exp ~loc (Lval ret) in
     let vals = assign ret rhs loc in
     (* Track referent numbers of assignments via function calls.
-       Realary functions (i.e., with no source code available) that return
+       Library functions (i.e., with no source code available) that return
        values are considered to be functions that allocate memory. They are
        considered so because they need to be handled exactly as memory
        allocating functions, that is, the referent of the returned pointer is
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 38dba48cbd257eaee239bede00fcb019f97fa272..b580ec514ff9a848344c975cba9101e73345d496 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -86,8 +86,7 @@ val join: number_ty -> number_ty -> number_ty
 (** {!number_ty} is a join-semi-lattice if you do not consider [Other]. If
     there is no [Other] in argument, this function computes the join of this
     semi-lattice. If one of the argument is {!Other}, the function assumes that
-    the other argument is also {!Other}. In this case, the result is [Other].
-    TODO: is now extended to support reals *)
+    the other argument is also {!Other}. In this case, the result is [Other]. *)
 
 (******************************************************************************)
 (** {2 Typing} *)