diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 6620c41a9b3e5d528d53541dfeff6cc7f01a27ec..0c1fd5a80c2f695d451f77944d4fd608bd6a25ac 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -387,13 +387,18 @@ sig
   val lc_term : term -> lc_term
   val lc_repr : lc_term -> term
 
-  (** {3 Recursion Scheme} *)
-
-  val e_map  : pool -> (term -> term) -> term -> term
-  (** Open and close binders *)
-
-  val e_iter : pool -> (term -> unit) -> term -> unit
-  (** Open binders *)
+  (** {3 Iteration Scheme} *)
+
+  val f_map  : ?pool:pool -> (term -> term) -> term -> term
+  (** Pass and open binders, maps its direct sub-terms
+      and then close then opened binders
+      Raises Invalid_argument in case of a bind-term without pool.
+      The optional pool must contain all free variables of the term. *)
+
+  val f_iter : ?pool:pool -> (term -> unit) -> term -> unit
+  (** Iterates over its direct sub-terms (pass and open binders)
+      Raises Invalid_argument in case of a bind-term without pool.
+      The optional pool must contain all free variables of the term. *)
 
   val lc_iter : (term -> unit) -> term -> unit
 
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 58b7ee820bfa69205a53a2afa6e396c8aad9ce89..a3e8ac03b507d732097566f1e18b9b8008865c08 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2354,22 +2354,26 @@ struct
 
   let lc_iter f e = repr_iter f e.repr
 
-  let e_map pool f e =
+  let f_map ?pool f e =
     match e.repr with
     | Apply(a,xs) -> e_apply (f a) (List.map f xs)
-    | Bind(q,t,e) ->
-        add_term pool e ;
-        let x = fresh pool t in
-        e_bind q x (f (lc_open x e))
+    | Bind _ ->
+        let pool = match pool with
+          | None -> raise (Invalid_argument "Qed.ogic.Term.f_map")
+          | Some pool -> pool in
+        let ctx,a = e_open pool e in
+        e_close ctx (rebuild f a)
     | _ -> rebuild f e
 
-  let e_iter pool f e =
+  let f_iter ?pool f e =
     match e.repr with
-    | Bind(_,t,e) ->
-        add_term pool e ;
-        let x = fresh pool t in
-        lc_iter f (lc_open x e)
-    | _ -> lc_iter f e
+    | Bind _ ->
+        let pool = match pool with
+          | None -> raise (Invalid_argument "Qed.ogic.Term.f_iter")
+          | Some pool -> pool in
+        let _,a = e_open pool e in
+        f a
+    | _ -> repr_iter f e.repr
 
   (* -------------------------------------------------------------------------- *)
   (* --- Sub-terms                                                          --- *)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index d567a02694dfdc0e833f7eef515b4097bd01ebbf..d3c3677929e400d65bdd1bd1169bf60e72fed715 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -950,7 +950,7 @@ let is_cint_simplifier = object (self)
             with Not_found -> t
           end
       | Imply (l1,l2) -> e_imply (List.map (walk ~is_goal:false) l1) (walk ~is_goal l2)
-      | _ -> Lang.F.QED.e_map pool (walk ~is_goal) t in
+      | _ -> Lang.F.QED.f_map ~pool (walk ~is_goal) t in
     Lang.F.p_bool (walk ~is_goal (Lang.F.e_prop p))
 
   method simplify_exp (e : term) = e