diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 91272859fed9fe8acd1018524fa3d252f2190063..5721069a0375d47aa0bc370ed84935a713a27922 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -225,10 +225,7 @@ let rec tau_of_ltype t =
   | Ltype _ as b when Logic_const.is_boolean_type b -> Logic.Bool
   | Ltype(lt,lts) -> atype lt (List.map tau_of_ltype lts)
 
-let tau_of_li_type ltype =
-  match ltype with
-  | None -> Logic.Prop
-  | Some t -> tau_of_ltype t
+let tau_of_return = function None -> Logic.Prop | Some t -> tau_of_ltype t
 
 (* -------------------------------------------------------------------------- *)
 (* --- Datatypes                                                          --- *)
@@ -420,7 +417,7 @@ and source =
 
 let tau_of_lfun phi ts =
   match phi with
-  | ACSL f -> tau_of_li_type f.l_type
+  | ACSL f -> tau_of_return f.l_type
   | CTOR c ->
     if c.ctor_type.lt_params = [] then Logic.Data(Atype c.ctor_type,[])
     else raise Not_found
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 4c196d1fa5e4f9c1c4773992c784423c7421c184..0dbdfa312a751ea09fa9ca548877069f07410d13 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -158,7 +158,7 @@ val extern_t:
 val tau_of_object : c_object -> tau
 val tau_of_ctype : typ -> tau
 val tau_of_ltype : logic_type -> tau
-val tau_of_li_type : logic_type option -> tau
+val tau_of_return : logic_type option -> tau
 val tau_of_lfun : lfun -> tau option list -> tau
 val tau_of_field : field -> tau
 val tau_of_record : field -> tau
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 34148ea36955964e78884dfec6ec41793e223a50..ffb93c239c4c2605f83b4b6ba2dd7513a2203c4e 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -440,7 +440,7 @@ struct
     let frame = logic_frame name types in
     in_frame frame
       begin fun () ->
-        let tres = Lang.tau_of_li_type tres in
+        let tres = Lang.tau_of_return tres in
         let env,domain,sigv = profile_env Logic_var.Map.empty [] [] profile in
         let env = default_label env labels in
         let result = cc env data in
@@ -563,7 +563,7 @@ struct
     in_frame frame
       begin fun () ->
         let lfun = ACSL l in
-        let tau = Lang.tau_of_li_type l.l_type in
+        let tau = Lang.tau_of_return l.l_type in
         let parp,sigp = Lang.local profile_sig l.l_profile in
         let ldef = {
           d_lfun = lfun ;
@@ -586,7 +586,7 @@ struct
     in_frame frame
       begin fun () ->
         let lfun = ACSL l in
-        let tau = Lang.tau_of_li_type l.l_type in
+        let tau = Lang.tau_of_return l.l_type in
         let parm,sigm = Lang.local (profile_mem l) vars in
         let ldef = {
           d_lfun = lfun ;