diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index b9d1954e66c90885377d0a694dabc8257fcbf32b..2d8c1789b5aa02a4d5b0ba050dfb5da2ee54536f 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -230,6 +230,7 @@ wp-doc-api:
 	$(CP) $(Wp_DIR)/doc/ocamldoc.css $(Wp_DIR)/doc/html/style.css
 	$(OCAMLDOC) \
 		-package zarith \
+		-package why3 \
 		-I lib/fc -I lib/plugins -I $(Wp_DIR) -stars \
 		-html -d $(Wp_DIR)/doc/html -charset utf-8 \
 		-t "Frama-C/WP API Documentation" \
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 3297bfdd33e5d765bec98e4957292dc31982f31a..44c812ddf3fe57936b2f4f7845ee511cb1dbdba6 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -292,8 +292,8 @@ let r_havoc = function
   | _ -> raise Not_found
 
 (* havoc(undef,m,p,a)[k] =
-   - undef[k]      WHEN separated (p,a,k,1)
-   - m[k]  WHEN NOT separated (p,a,k,1)
+   - m[k]     WHEN separated (p,a,k,1)
+   - undef[k] WHEN NOT separated (p,a,k,1)
 *)
 let r_get_havoc = function
   | [undef;m;p;a] ->
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index c0148af7dad77a5083a382d34de979efc203ca23..814f165a9b918d4431b257a06ea99520472803ca 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -933,16 +933,16 @@ struct
   let frame sigma =
     let hs = ref [] in
     SIGMA.iter
-     begin fun x chunk ->
-       (if (x.vglob || x.vformal) then
-          let t = VAR.typ_of_chunk x in
-          let v = e_var chunk in
-          let h = forall_pointers (M.global sigma.mem) v t in
-          if not (F.eqp h F.p_true) then hs := h :: !hs ) ;
-       (if x.vglob then
-          let v = e_var chunk in
-          hs := Cvalues.has_ctype x.vtype v :: !hs ) ;
-     end sigma.vars ;
+      begin fun x chunk ->
+        (if (x.vglob || x.vformal) then
+           let t = VAR.typ_of_chunk x in
+           let v = e_var chunk in
+           let h = forall_pointers (M.global sigma.mem) v t in
+           if not (F.eqp h F.p_true) then hs := h :: !hs ) ;
+        (if x.vglob then
+           let v = e_var chunk in
+           hs := Cvalues.has_ctype x.vtype v :: !hs ) ;
+      end sigma.vars ;
     !hs @ M.frame sigma.mem
 
   (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index 9e68996a899b6602601fc6334b8daa46eaa4e600..2f70cab4b56e27967b5eb34db7934388d945ce3e 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/src/plugins/wp/TacHavoc.ml
@@ -35,8 +35,8 @@ let lookup_havoc e =
   | L.Aget( m , p ) ->
       begin
         match F.repr m with
-        | L.Fun( f , [mr;m0;a;n] ) when f == MemMemory.f_havoc ->
-            Some( mr , m0 , a , n , p )
+        | L.Fun( f , [m_undef;m_sep;a;n] ) when f == MemMemory.f_havoc ->
+            Some( m_undef , m_sep , a , n , p )
         | _ -> None
       end
   | _ -> None