diff --git a/TODO b/TODO
index 635f5797ed2a39ea3ee8ba725e267b94c792a070..fea6d117d5f98bfd7dbd109bfe66be320f2ee2d1 100644
--- a/TODO
+++ b/TODO
@@ -1,3 +1,14 @@
+WhyML
+-----
+
+  - should the API ensure that every psymbol resets the new regions?
+    Should they be always reset at the last arrow? What if they are
+    already reset at some earlier arrows, should we reset them again?
+
+  - in "val" and "any", when a region rho is written into, but some
+    subregion rho' of rho is not, should we reset rho' under rho?
+    In Mlw_typing or in Mlw_expr?
+
 
 syntaxe
 -------
@@ -13,10 +24,10 @@ syntaxe
        match ... with 0 :: r -> ... | ...
 
 
-sémantique
+sémantique
 ----------
 
-  - env should not contain theories under the null path. 
+  - env should not contain theories under the null path.
     The current implementation of Typing.find_theory is potentially broken.
 
   - should split_goal provide a "right-hand side only split"?
@@ -28,16 +39,16 @@ s
     is not changed by a transformation, it will stay in the hash table forever,
     since the key is the value. Should we use generation numbers in arguments
     and results of transformations?
-     François -- I don't get that point the weak Hashtbl that we use
+     François -- I don't get that point the weak Hashtbl that we use
    are designed to work on this case, even with the identity function.
    What we should do is a way to remove the task from a session when
    they are not needed anymore.
 
-  - uses : pour l'instant, l'ordre des théories dans le fichier est important 
-    i.e. les théories mentionnées par uses doivent être définies précédemment
+  - uses : pour l'instant, l'ordre des théories dans le fichier est important
+    i.e. les théories mentionnées par uses doivent être définies précédemment
 
-  - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole 
-    de même nom)
+  - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole
+    de même nom)
 
 error reporting
 ---------------
@@ -60,4 +71,4 @@ tools
    than reported in the configuration
   - Maybe : make something generic for the dialog box with memory.
   - autodetection can be modified now that only name/version/altern
-   are taken into account in session.
\ No newline at end of file
+   are taken into account in session.
diff --git a/src/whyml/mlw_expr.ml b/src/whyml/mlw_expr.ml
index b9882a315afd31606da54483f7c1a8ab5043d929..a01810a1ce0d9475d41b0e23bb2630dec2441d37 100644
--- a/src/whyml/mlw_expr.ml
+++ b/src/whyml/mlw_expr.ml
@@ -214,7 +214,11 @@ let spec_vars varm variant pre post xpost eff result =
     raise (UnboundException (Sexn.choose badex));
   Mvs.fold (fun vs _ m -> add_vs_vars vs m) vsset varm
 
+exception DuplicateArg of pvsymbol
+
 let spec_arrow pvl effect vty =
+  let add pv s = Spv.add_new (DuplicateArg pv) pv s in
+  ignore (List.fold_right add pvl Spv.empty);
   let arg,argl = match List.rev pvl with
     | [] -> Loc.errorm "Empty argument list"
     | arg::argl -> arg, argl in
@@ -460,6 +464,7 @@ type expr = {
   e_vars   : varset Mid.t;
   e_label  : Slab.t;
   e_loc    : Loc.position option;
+  e_tag    : Hashweak.tag;
 }
 
 and expr_node =
@@ -502,6 +507,16 @@ and lambda = {
   l_xpost   : xpost;
 }
 
+module WSexpr = WeakStructMake (struct
+  type t = expr
+  let tag expr = expr.e_tag
+end)
+
+module Sexpr = WSexpr.S
+module Mexpr = WSexpr.M
+module Hexpr = WSexpr.H
+module Wexpr = WSexpr.W
+
 (* smart constructors *)
 
 let e_label ?loc l e = { e with e_label = l; e_loc = loc }
@@ -516,15 +531,24 @@ let e_label_copy { e_label = lab; e_loc = loc } e =
 exception GhostWrite of expr * region
 exception GhostRaise of expr * xsymbol
 
-let mk_expr node vty eff vars = {
+let mk_expr node vty eff vars c = {
   e_node   = node;
   e_vty    = vty;
   e_effect = if vty_ghost vty then eff_ghostify eff else eff;
   e_vars   = vars;
   e_label  = Slab.empty;
   e_loc    = None;
+  e_tag    = Hashweak.create_tag c;
 }
 
+let mk_expr =
+  let c = ref 0 in fun node vty eff vars ->
+    incr c; mk_expr node vty eff vars !c
+
+(* FIXME? e_label calls do not refresh the tag. This is safe
+   as long as we only use tags for "semantical things" such as
+   extended specification storage in WPs. *)
+
 let add_t_vars t m = Mvs.fold (fun vs _ m -> add_vs_vars vs m) t.t_vars m
 let add_e_vars e m = varmap_union e.e_vars m
 
diff --git a/src/whyml/mlw_expr.mli b/src/whyml/mlw_expr.mli
index cf3403c02c9f7a0e85321d8658e90161a2eaf40a..f91ebd53a0bdb853926c0f979e72c5055d801d09 100644
--- a/src/whyml/mlw_expr.mli
+++ b/src/whyml/mlw_expr.mli
@@ -133,6 +133,7 @@ type val_decl = private {
 
 val create_val : Ident.preid -> type_v -> val_decl
 
+exception DuplicateArg of pvsymbol
 exception UnboundException of xsymbol
 
 (** patterns *)
@@ -177,6 +178,7 @@ type expr = private {
   e_vars   : varset Mid.t;
   e_label  : Slab.t;
   e_loc    : Loc.position option;
+  e_tag    : Hashweak.tag;
 }
 
 and expr_node = private
@@ -224,6 +226,11 @@ and variant = {
   v_rel  : lsymbol option; (* tau tau : prop *)
 }
 
+module Mexpr : Map.S with type key = expr
+module Sexpr : Mexpr.Set
+module Hexpr : Hashtbl.S with type key = expr
+module Wexpr : Hashweak.S with type key = expr
+
 val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
 val e_label_add : label -> expr -> expr
 val e_label_copy : expr -> expr -> expr
diff --git a/src/whyml/mlw_pretty.ml b/src/whyml/mlw_pretty.ml
index e75690c90979387c310c4d16993068eabc4c1aff..e337dc9432395ec95de3087354d2f501099a5b2a 100644
--- a/src/whyml/mlw_pretty.ml
+++ b/src/whyml/mlw_pretty.ml
@@ -470,5 +470,7 @@ let () = Exn_printer.register
   | Mlw_expr.UnboundException xs ->
       fprintf fmt "This function raises %a but does not \
         specify a post-condition for it" print_xs xs
+  | Mlw_expr.DuplicateArg pv ->
+      fprintf fmt "Argument %a is used twice" print_pv pv
   | _ -> raise exn
   end
diff --git a/src/whyml/mlw_wp.ml b/src/whyml/mlw_wp.ml
index 502f386eb410e36aed6c2cdac680504b2fcd3a64..cb504fd8511b3b67cfc158b1efc246983b84e57d 100644
--- a/src/whyml/mlw_wp.ml
+++ b/src/whyml/mlw_wp.ml
@@ -62,7 +62,9 @@ let vs_now = create_vsymbol (id_fresh "'now") ty_mark
 
 let ls_absurd = create_lsymbol (id_fresh "absurd") [] None
 let t_absurd  = ps_app ls_absurd []
+
 let mk_t_if f = t_if f t_bool_true t_bool_false
+let to_term t = if t.t_ty = None then mk_t_if t else t
 
 (* replace [at(t,'old)] with [at(t,lab)] everywhere in formula [f] *)
 let old_mark lab t = t_subst_single vs_old (t_var lab) t
@@ -92,29 +94,27 @@ let rec drop_at now m t = match t.t_node with
 (** Specifications *)
 
 let psymbol_spec_t : type_v Wps.t = Wps.create 17
+let e_apply_spec_t : type_c Wexpr.t = Wexpr.create 17
 
 let add_pv_varm pv m = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_vars m
 let add_pv_vars pv s = vars_union pv.pv_vtv.vtv_vars s
 
-let check_spec ps tyv =
-  let rec check vty tyv = match vty, tyv with
-    | VTvalue _, SpecV _ -> ()
-    | VTarrow vta, SpecA (_::(_::_ as pvl), tyc) ->
-        assert (eff_is_empty vta.vta_effect);
-        check vta.vta_result (SpecA (pvl, tyc))
-    | VTarrow vta, SpecA ([_], tyc) ->
-        let eff1 = vta.vta_effect in
-        let eff2 = tyc.c_effect in
-        assert (Sreg.equal eff1.eff_reads  eff2.eff_reads);
-        assert (Sreg.equal eff1.eff_writes eff2.eff_writes);
-        assert (Sexn.equal eff1.eff_raises eff2.eff_raises);
-        assert (Sreg.equal eff1.eff_ghostr eff2.eff_ghostr);
-        assert (Sreg.equal eff1.eff_ghostw eff2.eff_ghostw);
-        assert (Sexn.equal eff1.eff_ghostx eff2.eff_ghostx);
-        check vta.vta_result tyc.c_result
-    | _ -> assert false
-  in
-  check (VTarrow ps.ps_vta) tyv
+let rec check_spec vty tyv = match vty, tyv with
+  | VTvalue _, SpecV _ -> ()
+  | VTarrow vta, SpecA (_::(_::_ as pvl), tyc) ->
+      assert (eff_is_empty vta.vta_effect);
+      check_spec vta.vta_result (SpecA (pvl, tyc))
+  | VTarrow vta, SpecA ([_], tyc) ->
+      let eff1 = vta.vta_effect in
+      let eff2 = tyc.c_effect in
+      assert (Sreg.equal eff1.eff_reads  eff2.eff_reads);
+      assert (Sreg.equal eff1.eff_writes eff2.eff_writes);
+      assert (Sexn.equal eff1.eff_raises eff2.eff_raises);
+      assert (Sreg.equal eff1.eff_ghostr eff2.eff_ghostr);
+      assert (Sreg.equal eff1.eff_ghostw eff2.eff_ghostw);
+      assert (Sexn.equal eff1.eff_ghostx eff2.eff_ghostx);
+      check_spec vta.vta_result tyc.c_result
+  | _ -> assert false
 
 let rec filter_v ~strict varm vars = function
   | SpecA (pvl, tyc) ->
@@ -136,6 +136,50 @@ and filter_c ~strict varm vars tyc =
   end;
   { tyc with c_effect = effect; c_result = result }
 
+let add_psymbol_spec ~strict varm ps tyv =
+  let vars = Mid.fold (fun _ -> vars_union) varm vars_empty in
+  let tyv = filter_v ~strict varm vars tyv in
+  check_spec (VTarrow ps.ps_vta) tyv; (* TODO: prove and remove *)
+  Wps.set psymbol_spec_t ps tyv
+
+(* TODO? move spec_inst and subst to Mlw_expr? *)
+let vtv_full_inst sbs vtv =
+  vty_value ~ghost:vtv.vtv_ghost (ity_full_inst sbs vtv.vtv_ity)
+
+let pv_full_inst sbs pv =
+  create_pvsymbol (id_clone pv.pv_vs.vs_name) (vtv_full_inst sbs pv.pv_vtv)
+
+let rec spec_inst_v sbs tvm vsm = function
+  | SpecV vtv ->
+      SpecV (vtv_full_inst sbs vtv)
+  | SpecA (pvl,tyc) ->
+      let add m pv =
+        let nv = pv_full_inst sbs pv in
+        Mvs.add pv.pv_vs (t_var nv.pv_vs) m, nv in
+      let vsm, pvl = Util.map_fold_left add vsm pvl in
+      SpecA (pvl, spec_inst_c sbs tvm vsm tyc)
+
+and spec_inst_c sbs tvm vsm tyc =
+  let subst = t_ty_subst tvm vsm in {
+    c_pre    = subst tyc.c_pre;
+    c_effect = eff_full_inst sbs tyc.c_effect;
+    c_result = spec_inst_v sbs tvm vsm tyc.c_result;
+    c_post   = subst tyc.c_post;
+    c_xpost  = Mexn.map subst tyc.c_xpost; }
+
+let rec subst_v pv t = function
+  | SpecA (pvl,tyc) when not (List.exists (pv_equal pv) pvl) ->
+      SpecA (pvl, subst_c pv t tyc)
+  | tyv -> tyv
+
+and subst_c pv t tyc =
+  let subst = t_subst (Mvs.singleton pv.pv_vs t) in {
+    c_pre    = subst tyc.c_pre;
+    c_effect = tyc.c_effect;
+    c_result = subst_v pv t tyc.c_result;
+    c_post   = subst tyc.c_post;
+    c_xpost  = Mexn.map subst tyc.c_xpost; }
+
 let spec_lambda l tyv =
   let tyc = {
     c_pre    = l.l_pre;
@@ -145,81 +189,104 @@ let spec_lambda l tyv =
     c_xpost  = l.l_xpost } in
   SpecA (l.l_args, tyc)
 
-let spec_val { val_name = lv; val_spec = tyv } = match lv with
-  | LetA ps when not (Wps.mem psymbol_spec_t ps) ->
-      check_spec ps tyv; (* TODO: remove *)
-      Wps.set psymbol_spec_t ps tyv
-  | _ -> ()
-
-let rec spec_let ~strict { let_var = lv; let_expr = e } = match lv with
-  | LetA ps when not (Wps.mem psymbol_spec_t ps) ->
-    (* FIXME: memoization is broken if one declares the same psymbol
-       both as a local (non-strict) let and as a global (strict) let.
-       First global, then local is safe. First local, then global
-       may lead to an escaping variable, which will or will not
-       be detected by the core API. *)
-      let vars = Mid.fold (fun _ -> vars_union) e.e_vars vars_empty in
-      let tyv = filter_v ~strict e.e_vars vars (spec_expr e) in
-      check_spec ps tyv; (* TODO: remove *)
-      Wps.set psymbol_spec_t ps tyv
-  | _ -> ()
-
-and spec_rec rdl =
+let spec_val vd = match vd.val_name with
+  | LetA ps -> add_psymbol_spec ~strict:true vd.val_vars ps vd.val_spec
+  | LetV _  -> ()
+
+let rec spec_let ~strict pvm { let_var = lv; let_expr = e } = match lv with
+  | LetA ps -> add_psymbol_spec ~strict e.e_vars ps (spec_expr pvm e)
+  | LetV _  -> ignore (spec_expr pvm e)
+
+and spec_rec pvm rdl =
   let add_vars m rd = Mid.set_union m rd.rec_vars in
   let vars = List.fold_left add_vars Mid.empty rdl in
   let add_early_spec rd = match rd.rec_lambda.l_expr.e_vty with
     | VTvalue vtv ->
         let tyv = spec_lambda rd.rec_lambda (SpecV vtv) in
-        check_spec rd.rec_ps tyv; (* TODO: remove *)
-        Wps.set psymbol_spec_t rd.rec_ps tyv
+        add_psymbol_spec ~strict:true rd.rec_vars rd.rec_ps tyv
     | VTarrow _ when Mid.mem rd.rec_ps.ps_name vars ->
         Loc.errorm ?loc:rd.rec_lambda.l_expr.e_loc
           "The body of a recursive function must be a first-order value"
     | VTarrow _ -> () in
   List.iter add_early_spec rdl;
   let add_late_spec rd =
-    let tyv = spec_expr rd.rec_lambda.l_expr in
+    let tyv = spec_expr pvm rd.rec_lambda.l_expr in
     match rd.rec_lambda.l_expr.e_vty with
     | VTarrow _ ->
         let tyv = spec_lambda rd.rec_lambda tyv in
-        check_spec rd.rec_ps tyv; (* TODO: remove *)
-        Wps.set psymbol_spec_t rd.rec_ps tyv
+        add_psymbol_spec ~strict:true rd.rec_vars rd.rec_ps tyv
     | VTvalue _ -> () in
   List.iter add_late_spec rdl
 
-and spec_expr e = match e.e_node with
+and spec_expr pvm e = match e.e_node with
   | Elogic _
   | Eassert _
   | Eabsurd -> SpecV (vtv_of_expr e)
   | Evalue pv -> SpecV pv.pv_vtv
-  | Earrow ps -> Wps.find psymbol_spec_t ps
-      (* TODO: a ps may not be in the table, if it comes from a module
-         for which we never computed WPs. Pass the known_map to spec_expr
-         and compute it now. *)
-  | Eapp (_, _) ->
-      assert false (* TODO *)
-  | Elet (ld,e1) -> spec_let ~strict:false ld; spec_expr e1
-  | Erec (rdl,e1) -> spec_rec rdl; spec_expr e1
-  | Eghost e1 -> spec_expr e1
+  | Earrow ps ->
+    (* TODO: a ps may not be in the table, if it comes from a module
+       for which we never computed WPs. Pass the known_map to spec_expr
+       and compute it now. *)
+      let rec vty_match sbs t1 t2 = match t1,t2 with
+        | VTvalue v1, VTvalue v2 ->
+            ity_match sbs v1.vtv_ity v2.vtv_ity
+        | VTarrow a1, VTarrow a2 ->
+            let sbs = ity_match sbs a1.vta_arg.vtv_ity a2.vta_arg.vtv_ity in
+            vty_match sbs a1.vta_result a2.vta_result
+        | _ -> assert false
+      in
+      let sbs = vty_match ps.ps_subst (VTarrow ps.ps_vta) e.e_vty in
+      let tvm = Mtv.map ty_of_ity sbs.ity_subst_tv in
+      let tyv = Wps.find psymbol_spec_t ps in
+      spec_inst_v sbs tvm Mvs.empty tyv
+  | Eapp (e1,pv) ->
+      let tyv = spec_expr pvm e1 in
+      let t = Mpv.find_def (t_var pv.pv_vs) pv pvm in
+      begin match tyv with
+        | SpecA ([pv],tyc) ->
+            let tyc = subst_c pv t tyc in
+            (* we will use this for WP *)
+            Wexpr.set e_apply_spec_t e tyc;
+            tyc.c_result
+        | SpecA (pv::pvl,tyc) ->
+            (* pv cannot occur in pvl *)
+            SpecA (pvl, subst_c pv t tyc)
+        | _ -> assert false
+      end
+  | Elet (ld,e1) ->
+      spec_let ~strict:false pvm ld;
+      let pvm = match ld.let_var, e1.e_node with
+        | LetV pv, Elogic t ->
+            Mpv.add pv (to_term t) pvm
+        | LetV pv, Evalue v ->
+            let t = Mpv.find_def (t_var v.pv_vs) v pvm in
+            Mpv.add pv t pvm
+        | _ -> pvm
+      in
+      spec_expr pvm e1
+  | Erec (rdl,e1) ->
+      spec_rec pvm rdl;
+      spec_expr pvm e1
+  | Eghost e1 -> spec_expr pvm e1
   | Eany tyc -> tyc.c_result
   | Eassign (e1,_,_)
   | Eloop (_,_,e1)
   | Efor (_,_,_,e1)
   | Eraise (_,e1)
   | Eabstr (e1,_,_) ->
-      ignore (spec_expr e1);
+      ignore (spec_expr pvm e1);
       SpecV (vtv_of_expr e)
   | Eif (e1,e2,e3) ->
-      ignore (spec_expr e1);
-      ignore (spec_expr e2);
-      spec_expr e3
+      ignore (spec_expr pvm e1);
+      ignore (spec_expr pvm e2);
+      spec_expr pvm e3
   | Ecase (e1,bl) ->
-      ignore (spec_expr e1);
-      List.iter (fun (_,e) -> ignore (spec_expr e)) bl;
+      ignore (spec_expr pvm e1);
+      List.iter (fun (_,e) -> ignore (spec_expr pvm e)) bl;
       SpecV (vtv_of_expr e)
   | Etry (e1,bl) ->
-      ignore (spec_expr e1);
-      List.iter (fun (_,_,e) -> ignore (spec_expr e)) bl;
+      ignore (spec_expr pvm e1);
+      List.iter (fun (_,_,e) -> ignore (spec_expr pvm e)) bl;
       SpecV (vtv_of_expr e)
 
 (** WP utilities *)
@@ -246,10 +313,10 @@ let wp_expl l f =
   let lab = Slab.add (Ident.create_label ("expl:" ^ l)) lab in
   t_label ?loc:f.t_loc lab f
 
-let wp_and ?(sym=false) f1 f2 =
+let wp_and ~sym f1 f2 =
   if sym then t_and_simp f1 f2 else t_and_asym_simp f1 f2
 
-let wp_ands ?(sym=false) fl =
+let wp_ands ~sym fl =
   if sym then t_and_simp_l fl else t_and_asym_simp_l fl
 
 let wp_implies f1 f2 = t_implies_simp f1 f2
@@ -378,6 +445,12 @@ let regs_of_reads  eff = Sreg.union eff.eff_reads eff.eff_ghostr
 let regs_of_writes eff = Sreg.union eff.eff_writes eff.eff_ghostw
 let regs_of_effect eff = Sreg.union (regs_of_reads eff) (regs_of_writes eff)
 
+let t_void = fs_app (fs_tuple 0) [] ty_unit
+
+let open_unit_post q =
+  let v, q = open_post q in
+  t_subst_single v t_void q
+
 let rec wp_expr env e q xq =
   let lab = fresh_mark () in
   let q = old_mark lab q in
@@ -395,21 +468,32 @@ and wp_desc env e q xq = match e.e_node with
   | Elogic t ->
       let v, q = open_post q in
       let t = wp_label e t in
-      let t = if t.t_ty = None then mk_t_if t else t in
-      t_subst_single v t q
+      t_subst_single v (to_term t) q
   | Evalue pv ->
       let v, q = open_post q in
       let t = wp_label e (t_var pv.pv_vs) in
       t_subst_single v t q
+  | Earrow _ ->
+      let q = open_unit_post q in
+      (* wp_label e *) q (* FIXME? *)
   | Erec (rdl, e) ->
       let fr = wp_rec_defn env rdl in
       let fe = wp_expr env e q xq in
       wp_and ~sym:true (wp_ands ~sym:true fr) fe
+  | Eassert (Aassert, f) ->
+      let q = open_unit_post q in
+      let f = wp_expl "assertion" f in
+      wp_and ~sym:false (wp_label e f) q
+  | Eassert (Acheck, f) ->
+      let q = open_unit_post q in
+      let f = wp_expl "check" f in
+      wp_and ~sym:true (wp_label e f) q
+  | Eassert (Aassume, f) ->
+      let q = open_unit_post q in
+      wp_implies (wp_label e f) q
   | Eabsurd ->
       wp_label e t_absurd
 
-  |Earrow _-> assert false
-  |Eassert (_, _)-> assert false
   |Eabstr (_, _, _)-> assert false
   |Etry (_, _)-> assert false
   |Eraise (_, _)-> assert false
@@ -522,7 +606,7 @@ let mk_env env km th = {
 }
 
 let wp_let env km th ({ let_var = lv; let_expr = e } as ld) =
-  spec_let ~strict:true ld;
+  spec_let ~strict:true Mpv.empty ld;
   let env = mk_env env km th in
   let q, xq = default_post e.e_vty e.e_effect in
   let f = wp_expr env e q xq in
@@ -533,7 +617,7 @@ let wp_let env km th ({ let_var = lv; let_expr = e } as ld) =
   add_wp_decl id f th
 
 let wp_rec env km th rdl =
-  spec_rec rdl;
+  spec_rec Mpv.empty rdl;
   let env = mk_env env km th in
   let fl = wp_rec_defn env rdl in
   let add_one th d f =