diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 2c3dbf5058832c3cca154dcd2b5c66e52e9667b6..c4c9997e4698c8623f1f73a1f753272b7d59763d 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -186,7 +186,7 @@ let t_int = Logic.Int
 let t_bool = Logic.Bool
 let t_real = Logic.Real
 let t_prop = Logic.Prop
-let t_addr () = Context.get pointer Cil.voidType
+let t_addr () = Context.get pointer
 let t_array a = Logic.Array(Logic.Int,a)
 let t_farray a b = Logic.Array(a,b)
 let t_datatype adt ts = Logic.Data(adt,ts)
@@ -194,8 +194,8 @@ let t_datatype adt ts = Logic.Data(adt,ts)
 let rec tau_of_object = function
   | C_int _ -> Logic.Int
   | C_float f -> Context.get floats f
-  | C_pointer t -> Context.get pointer t
   | C_comp c -> tau_of_comp c
+  | C_pointer _ -> Context.get pointer
   | C_array { arr_element = typ } -> t_array (tau_of_ctype typ)
 
 and tau_of_ctype typ = tau_of_object (Ctypes.object_of typ)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index ac60a9778810dc3dc647e0b653c83732abc4358c..d8a13b4ad92c65316dc974232a83d8ff81247392 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -177,12 +177,12 @@ val t_int : tau
 val t_real : tau
 val t_bool : tau
 val t_prop : tau
-val t_addr : unit -> tau (** pointer on Void *)
+val t_addr : unit -> tau
 val t_array : tau -> tau
 val t_farray : tau -> tau -> tau
 val t_datatype : adt -> tau list -> tau
 
-val pointer : (typ -> tau) Context.value (** type of pointers *)
+val pointer : tau Context.value (** type of pointers *)
 val floats : (c_float -> tau) Context.value (** type of floats *)
 val poly : string list Context.value (** polymorphism *)
 val builtin_types: (string -> t_builtin) Context.value (* builtin types *)
diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index 837d3f28f39ba069e34cc8093e574fb97cedc744..1edfc12dcab461720cf3ec55016ba44aacfadb89 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -32,7 +32,7 @@ module Logic = Qed.Logic
 let datatype = "MemEmpty"
 let configure () =
   begin
-    let orig_pointer = Context.push Lang.pointer (fun _typ -> Logic.Int) in
+    let orig_pointer = Context.push Lang.pointer Logic.Int in
     let orig_null    = Context.push Cvalues.null (p_equal e_zero) in
     let rollback () =
       Context.pop Lang.pointer orig_pointer ;
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index eabf76e10906d2d1e513d1506aacc32776cd1727..2f1cdc6a8563bd5298acfc2c61165a92b5590638 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -428,7 +428,7 @@ let datatype = "MemRegion"
 
 let configure () =
   begin
-    let orig_pointer = Context.push Lang.pointer (fun _ -> t_index) in
+    let orig_pointer = Context.push Lang.pointer t_index in
     let orig_null = Context.push Cvalues.null p_inull in
     let rollback () =
       Context.pop Lang.pointer orig_pointer ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index b885cd1e214cbe39054649bf0aee6a2974d2116f..36c8e0facd506e96b6ce47b3a9e67ab53fe9546b 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -45,7 +45,7 @@ let datatype = "MemTyped"
 let hypotheses p = p
 let configure () =
   begin
-    let orig_pointer = Context.push Lang.pointer (fun _ -> t_addr) in
+    let orig_pointer = Context.push Lang.pointer t_addr in
     let orig_null    = Context.push Cvalues.null (p_equal a_null) in
     let rollback () =
       Context.pop Lang.pointer orig_pointer ;
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 4bd0f123fe21fb704e8ea1f653a52364e0c23e41..6706a5a6f194fc3767189e66f288eb3ea5eb8222 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1056,6 +1056,7 @@ struct
           initialized_loc sigma obj x ofs
         in
         Lang.F.p_conj (List.map mk_pred ci.cfields)
+
   and initialized_range sigma obj x ofs low up =
     match obj with
     | C_array { arr_element=t } ->
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index 3e185883a6dc47ecbf239c9a312ab8b8bbc1efcf..ebfae47bf09c5fddcd2f80bb06b6adc478061602 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -36,7 +36,7 @@ let datatype = "MemZeroAlias"
 
 let configure () =
   begin
-    let orig_pointer = Context.push Lang.pointer (fun _typ -> Logic.Int) in
+    let orig_pointer = Context.push Lang.pointer Logic.Int in
     let orig_null    = Context.push Cvalues.null (p_equal e_zero) in
     let rollback () =
       Context.pop Lang.pointer orig_pointer ;