diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 51dac6a97767622f11be304e0b7f9dd1ed7d37c1..60cb51183feb0ef57b62634ca64b5d59de5b28d1 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,10 +15,13 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+- E-ACSL	[2012/01/20] Use GMP arithmetics only when required
+	        (i.e. mostly never in practice).
+
 ###################################
 Plugin E-ACSL 0.1 Nitrogen_20111001
 ###################################
 
--  E-ACSL         [2012/01/06] First release for the Hi-Lite FUI9 project.
+- E-ACSL	[2012/01/06] First release for the Hi-Lite FUI9 project.
 
 ###################################
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 428c76dd7aa24fcb83ecce6f6e025a6295bf3a55..7e2859479b4a991980298711a4b66639967be309 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -29,7 +29,7 @@ module BI = My_bigint
 let is_representable n _k _s = BI.ge n BI.min_int64 && BI.le n BI.max_int64
 
 (******************************************************************************)
-(** Type Lattice *)
+(** Type Definitions: Intervals *)
 (******************************************************************************)
 
 type eacsl_typ =
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index d843afe365017eb1e4175d65e660d11435a36473..9af55e88bd2e62a9ed1159151b6a1677421798ca 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -26,21 +26,37 @@ open Cil_types
 (** {2 Typing} *)
 (******************************************************************************)
 
-val typ_of_term: term -> typ
 val type_named_predicate: predicate named -> unit
+(** Compute the type of each term of the given predicate. *)
+
 val type_term: term -> unit
+(** Compute the type of the given term. *)
+
+val typ_of_term: term -> typ
+(** Get the type of the given term. Must have been previously computed. *)
+
 val unsafe_set_term: term -> typ -> unit
+(** Modify the type of the given term. No verification is done to check that the
+    new type is correct. *)
+
 val clear: unit -> unit
+(** Remove all the previously computed types. *)
 
 (******************************************************************************)
 (** {2 Subtyping} *)
 (******************************************************************************)
 
 val principal_type: term -> term -> typ
+(** Get the principal type of the two given terms, that is the type which may
+    contain both of them. Their types must have been previously computed. *)
 
 val context_sensitive: 
   ?loc:location -> Env.t -> typ -> bool -> term option -> exp -> 
   exp * Env.t
+(** [context_sensitive env ty is_mpz_string t_opt e] converts [e] in [env] in
+    such a way that it becomes usable in a context of type [ty]. [t_opt], if
+    any, is a term denoting by [e]. [is_mpz_string] is [true] iff [e] is a
+    string denoting a MPZ integer. *)
 
 val is_representable: My_bigint.t -> ikind -> string option -> bool
 (** Is the given constant representable?
@@ -53,6 +69,8 @@ val is_representable: My_bigint.t -> ikind -> string option -> bool
 val compute_quantif_guards_ref
     : (predicate named -> logic_var list -> predicate named -> 
        (term * relation * logic_var * relation * term) list) ref
+(** Forward reference. *)
+
 
 (*
 Local Variables: