--- ./src/wp/share/why3/Memory.v.orig	2014-03-12 09:07:51.000000000 -0600
+++ ./src/wp/share/why3/Memory.v	2014-09-06 21:30:00.000000000 -0600
@@ -137,29 +137,29 @@ Definition separated (p:addr) (a:Z) (q:a
   (((offset p) + a)%Z <= (offset q))%Z))).
 
 (* Why3 assumption *)
-Definition eqmem {a:Type} {a_WT:WhyType a} (m1:(@map.Map.map
-  addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT))
-  (p:addr) (a1:Z): Prop := forall (q:addr), (included q 1%Z p a1) ->
+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)).
 
 (* Why3 assumption *)
-Definition havoc {a:Type} {a_WT:WhyType a} (m1:(@map.Map.map
-  addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT))
-  (p:addr) (a1:Z): Prop := forall (q:addr), (separated q 1%Z p a1) ->
+Definition havoc {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), (separated q 1%Z p a1) ->
   ((map.Map.get m1 q) = (map.Map.get m2 q)).
 
 (* Why3 assumption *)
-Definition valid_rd (m:(@map.Map.map Z _ Z _)) (p:addr) (n:Z): Prop :=
+Definition valid_rd (m:(map.Map.map Z Z)) (p:addr) (n:Z): Prop :=
   (0%Z < n)%Z -> ((0%Z <= (offset p))%Z /\
   (((offset p) + n)%Z <= (map.Map.get m (base p)))%Z).
 
 (* Why3 assumption *)
-Definition valid_rw (m:(@map.Map.map Z _ Z _)) (p:addr) (n:Z): Prop :=
+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)).
 
 (* Why3 goal *)
-Lemma valid_rw_rd : forall (m:(@map.Map.map Z _ Z _)), forall (p:addr),
+Lemma valid_rw_rd : forall (m:(map.Map.map Z Z)), forall (p:addr),
   forall (n:Z), (valid_rw m p n) -> (valid_rd m p n).
 intros m p n.
 unfold valid_rw. unfold valid_rd.
@@ -167,7 +167,7 @@ intuition (auto with zarith).
 Qed.
 
 (* Why3 goal *)
-Lemma valid_string : forall (m:(@map.Map.map Z _ Z _)), forall (p:addr),
+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) /\
   ~ (valid_rw m p 1%Z))).
@@ -227,17 +227,17 @@ Definition region: Z -> Z.
 Admitted.
 
 (* Why3 goal *)
-Definition linked: (@map.Map.map Z _ Z _) -> Prop.
+Definition linked: (map.Map.map Z Z) -> Prop.
 Admitted.
 
 (* Why3 goal *)
-Definition sconst: (@map.Map.map addr addr_WhyType Z _) -> Prop.
+Definition sconst: (map.Map.map addr Z) -> Prop.
 Admitted.
 
 (* Why3 assumption *)
-Definition framed (m:(@map.Map.map addr addr_WhyType
-  addr addr_WhyType)): Prop := forall (p:addr), ((region (base (map.Map.get m
-  p))) <= 0%Z)%Z.
+Definition framed (m:(map.Map.map addr addr)): Prop :=
+  forall (p:addr), ((region (base (map.Map.get m p (a_WT := addr_WhyType)
+  (b_WT := addr_WhyType)))) <= 0%Z)%Z.
 
 (* Why3 goal *)
 Lemma separated_included : forall (p:addr) (q:addr), forall (a:Z) (b:Z),
@@ -283,22 +283,22 @@ Qed.
 
 (* Why3 goal *)
 Lemma eqmem_included : forall {a:Type} {a_WT:WhyType a},
-  forall (m1:(@map.Map.map addr addr_WhyType a a_WT)) (m2:(@map.Map.map
-  addr addr_WhyType a a_WT)), forall (p:addr) (q:addr), forall (a1:Z) (b:Z),
+  forall (m1:(map.Map.map addr a)) (m2:(map.Map.map addr a)),
+  forall (p:addr) (q:addr), forall (a1:Z) (b:Z),
   (included p a1 q b) -> ((eqmem m1 m2 q b) -> (eqmem m1 m2 p a1)).
 intros a a_WT m1 m2 p q a1 b h1 h2.
 Admitted.
 
 (* Why3 goal *)
-Lemma eqmem_sym : forall {a:Type} {a_WT:WhyType a}, forall (m1:(@map.Map.map
-  addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT)),
+Lemma eqmem_sym : forall {a:Type} {a_WT:WhyType a},
+  forall (m1:(map.Map.map addr a)) (m2:(map.Map.map addr a)),
   forall (p:addr), forall (a1:Z), (eqmem m1 m2 p a1) -> (eqmem m2 m1 p a1).
  intros A m1 m2 p a. unfold eqmem.
 Admitted.
 
 (* Why3 goal *)
-Lemma havoc_sym : forall {a:Type} {a_WT:WhyType a}, forall (m1:(@map.Map.map
-  addr addr_WhyType a a_WT)) (m2:(@map.Map.map addr addr_WhyType a a_WT)),
+Lemma havoc_sym : forall {a:Type} {a_WT:WhyType a},
+  forall (m1:(map.Map.map addr a)) (m2:(map.Map.map addr a)),
   forall (p:addr), forall (a1:Z), (havoc m1 m2 p a1) -> (havoc m2 m1 p a1).
 Admitted.
 
--- ./src/wp/share/why3/Qedlib.v.orig	2014-03-12 09:07:51.000000000 -0600
+++ ./src/wp/share/why3/Qedlib.v	2014-09-06 21:00:00.000000000 -0600
@@ -187,13 +187,14 @@ Definition real_hex := real_base 2%R.
 
 Record farray (A B : Type) := { whytype1 : BuiltIn.WhyType A ;
                                whytype2 : BuiltIn.WhyType B ;
-                               access :> @Map.map A whytype1 B whytype2 }.
+                               access :> Map.map A B }.
 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 m k.
+  (m : farray A B) (k : A) : B := Map.get m k
+  (a_WT := whytype1 m) (b_WT := whytype2 m).
 
 Lemma farray_eq : forall A B (m1 m2 : farray A B),
    whytype1 m1 = whytype1 m2 -> whytype2 m1 = whytype2 m2 ->
@@ -210,7 +211,8 @@ 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 m k v|}.
+  {| whytype1 := whytype1 m; whytype2 := whytype2 m;
+     access := Map.set m k v (a_WT := whytype1 m) (b_WT := whytype2 m) |}.
 
 Notation " a .[ k ] " := (select a k) (at level 60).
 Notation " a .[ k <- v ] " := (update a k v) (at level 60).