diff --git a/src/plugins/wp/share/why3/Bits.v b/src/plugins/wp/share/why3/Bits.v
index 0381e15181d8c41bcc35734f624d9fe24be8dfa4..624a253f499923ab9206ce27fe7bd78ca4313ce8 100644
--- a/src/plugins/wp/share/why3/Bits.v
+++ b/src/plugins/wp/share/why3/Bits.v
@@ -587,7 +587,7 @@ Qed.
 (** {@integer:} *)
 (** * Bits of Integers *)
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (** The bits representation of an integer consists of a bit function,
     packed with its trailing property. 
diff --git a/src/plugins/wp/share/why3/Cbits.v b/src/plugins/wp/share/why3/Cbits.v
index aff75e9b1e9667a2d0cf74393c4fae83a97721f2..c32a1cf32a5ab401e78c78dae72c60082d138dfd 100644
--- a/src/plugins/wp/share/why3/Cbits.v
+++ b/src/plugins/wp/share/why3/Cbits.v
@@ -167,7 +167,7 @@ Proof.
 Qed.
 
 Require Import Qedlib.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (** * Bit extraction *)
 (** Tacticals *)
diff --git a/src/plugins/wp/share/why3/Cint.v b/src/plugins/wp/share/why3/Cint.v
index 3a7c0ab7042f7c00f5b022ea1231af44ac2904d5..1f80f9e6d3254d795bbfa37f0ff06dfb57d97db2 100644
--- a/src/plugins/wp/share/why3/Cint.v
+++ b/src/plugins/wp/share/why3/Cint.v
@@ -117,7 +117,7 @@ Proof.
 intros x. unfold to_bool. induction (Z.eqb_spec x 0%Z) ; intuition.
 Qed.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Definition to_range a b z := a + (z-a) mod (b-a).
 
@@ -328,7 +328,6 @@ Proof. to_range.
 Qed.
 
 (** * C-Integer Conversions are identity when in-range *)
-Open Local Scope Z_scope.
 
 Remark mod_kn_mod_n:  forall (k:Z) (n:Z) (x:Z), k>0 -> n>0 -> (x mod (k*n)) mod n = x mod n.
 Proof.
diff --git a/src/plugins/wp/share/why3/Memory.v b/src/plugins/wp/share/why3/Memory.v
index a8aa1ff53a88bac2c385d7bc61603d29ac53173f..a586724d831b0224f3aedf8d52b4c80f9f1549ed 100644
--- a/src/plugins/wp/share/why3/Memory.v
+++ b/src/plugins/wp/share/why3/Memory.v
@@ -143,7 +143,7 @@ Definition separated (p:addr) (a:Z) (q:addr) (b:Z): Prop := (a <= 0%Z)%Z \/
 (* Why3 assumption *)
 Definition eqmem {a:Type} {a_WT:WhyType a} (m1:(map.Map.map addr a))
   (m2:(map.Map.map addr a)) (p:addr) (a1:Z): Prop := forall (q:addr),
-  (included q 1%Z p a1) -> ((map.Map.get m1 q) = (map.Map.get m2 q)).
+  (included q 1%Z p a1) -> ((m1 q) = (m2 q)).
 
 (* Why3 goal *)
 Definition havoc: forall {a:Type} {a_WT:WhyType a}, (map.Map.map addr a) ->
@@ -160,16 +160,16 @@ Definition fhavoc {A : Type}
 (* Why3 assumption *)
 Definition valid_rw (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
   (0%Z < n)%Z -> ((0%Z < (base p))%Z /\ ((0%Z <= (offset p))%Z /\
-  (((offset p) + n)%Z <= (map.Map.get m (base p)))%Z)).
+  (((offset p) + n)%Z <= (m (base p)))%Z)).
 
 (* Why3 assumption *)
 Definition valid_rd (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
   (0%Z < n)%Z -> ((~ (0%Z = (base p))) /\ ((0%Z <= (offset p))%Z /\
-  (((offset p) + n)%Z <= (map.Map.get m (base p)))%Z)).
+  (((offset p) + n)%Z <= (m (base p)))%Z)).
 
 (* Why3 assumption *)
 Definition invalid (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
-  (0%Z < n)%Z -> (((map.Map.get m (base p)) <= (offset p))%Z \/
+  (0%Z < n)%Z -> (((m (base p)) <= (offset p))%Z \/
   (((offset p) + n)%Z <= 0%Z)%Z).
 
 (* Why3 goal *)
@@ -184,7 +184,7 @@ Qed.
 (* Why3 goal *)
 Lemma valid_string : forall (m:(map.Map.map Z Z)), forall (p:addr),
   ((base p) < 0%Z)%Z -> (((0%Z <= (offset p))%Z /\
-  ((offset p) < (map.Map.get m (base p)))%Z) -> ((valid_rd m p 1%Z) /\
+  ((offset p) < (m (base p)))%Z) -> ((valid_rd m p 1%Z) /\
   ~ (valid_rw m p 1%Z))).
 Proof.
   intros m p.
@@ -251,7 +251,7 @@ Admitted.
 
 (* Why3 assumption *)
 Definition framed (m:(map.Map.map addr addr)): Prop := forall (p:addr),
-  ((region (base (map.Map.get m p))) <= 0%Z)%Z.
+  ((region (base (m p))) <= 0%Z)%Z.
 
 (* Why3 goal *)
 Lemma separated_included : forall (p:addr) (q:addr), forall (a:Z) (b:Z),
@@ -318,9 +318,9 @@ Admitted.
 (* Why3 goal *)
 Lemma havoc_access : forall {a:Type} {a_WT:WhyType a},
   forall (m0:(map.Map.map addr a)) (m1:(map.Map.map addr a)), forall (q:addr)
-  (p:addr), forall (a1:Z), ((separated q 1%Z p a1) -> ((map.Map.get (havoc m0
-  m1 p a1) q) = (map.Map.get m1 q))) /\ ((~ (separated q 1%Z p a1)) ->
-  ((map.Map.get (havoc m0 m1 p a1) q) = (map.Map.get m0 q))).
+  (p:addr), forall (a1:Z), ((separated q 1%Z p a1) -> (((havoc m0
+  m1 p a1) q) = (m1 q))) /\ ((~ (separated q 1%Z p a1)) ->
+  (((havoc m0 m1 p a1) q) = (m0 q))).
 Proof.
   intros a a_WT m0 m1 q p a1.
 Admitted.
diff --git a/src/plugins/wp/share/why3/Qedlib.v b/src/plugins/wp/share/why3/Qedlib.v
index 4156a9e32907453de88b7494189f01dd8ce715ea..68c2a998c3dd04aefa90a44182940d74a305771c 100644
--- a/src/plugins/wp/share/why3/Qedlib.v
+++ b/src/plugins/wp/share/why3/Qedlib.v
@@ -211,8 +211,9 @@ Definition array (A : Type) := farray Z A.
 Hypothesis extensionality: forall (A B : Type) (f g : A -> B),
   (forall x, f x = g x) -> f = g.
 
+
 Definition select {A B : Type}
-  (m : farray A B) (k : A) : B := @Map.get A (whytype1 m) B (whytype2 m) m k.
+  (m : farray A B) (k : A) : B := (access m k).
 
 Lemma farray_eq : forall A B (m1 m2 : farray A B),
    whytype1 m1 = whytype1 m2 -> whytype2 m1 = whytype2 m2 ->
@@ -221,15 +222,14 @@ Proof.
   intros A B m1 m2.
   destruct m1. destruct m2. simpl.
   intros H1 H2; rewrite H1; rewrite H2 ; clear H1 H2.
-  destruct access0. destruct access1. compute.
   intro K.
-  rewrite (extensionality b b0 K).
+  rewrite (extensionality access0 access1 K).
   reflexivity.
 Qed.
 
 Definition update {A B : Type}
   (m : farray A B) (k : A) (v : B) : (farray A B) :=
-  {| whytype1 := whytype1 m; whytype2 := whytype2 m; access := @Map.set A (whytype1 m) B (whytype2 m) m k v|}.
+  {| whytype1 := whytype1 m; whytype2 := whytype2 m; access := @Map.set A (whytype1 m) B (whytype2 m) (access m) k v|}.
 
 Notation " a .[ k ] " := (select a k) (at level 60).
 Notation " a .[ k <- v ] " := (update a k v) (at level 60).
@@ -239,7 +239,7 @@ Lemma access_update :
   m.[k <- v].[k] = v.
 Proof.
   intros.
-  apply Map.Select_eq.
+  apply Map.set_def.
   reflexivity.
 Qed.
 
@@ -248,8 +248,8 @@ Lemma access_update_neq :
   i <> j -> m.[ i <- v ].[j] = m.[j].
 Proof.
   intros.
-  apply Map.Select_neq.
-  assumption.
+  apply Map.set_def.
+  auto.
 Qed.
 
 (** ** Division on Z *)
diff --git a/src/plugins/wp/share/why3/Vlist.v b/src/plugins/wp/share/why3/Vlist.v
index 182898718639ae466b39a16277bcd32445f8be76..dfcb15ea7fdc389ba1e81e3e9e448e06fb84d7fc 100644
--- a/src/plugins/wp/share/why3/Vlist.v
+++ b/src/plugins/wp/share/why3/Vlist.v
@@ -64,7 +64,7 @@ Defined.
 Definition concat: forall {a:Type} {a_WT:WhyType a}, (list a) -> (list a) ->
   (list a).
   intros a a_WT.
-  Open Local Scope list_scope.
+  Local Open Scope list_scope.
   exact(fun u v => u ++ v).
 Defined.
 
diff --git a/src/plugins/wp/share/why3/Zbits.v b/src/plugins/wp/share/why3/Zbits.v
index e168e835e820688d375580f4521ecd7911399972..0c02116df5e35bf4555528819a49b1a7a504b4fa 100644
--- a/src/plugins/wp/share/why3/Zbits.v
+++ b/src/plugins/wp/share/why3/Zbits.v
@@ -46,7 +46,7 @@ Require Import Qedlib.
 Require Import Bits.
 Require Import Psatz.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Local Ltac omegaContradiction := cut False; [contradiction|omega].