diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 94ce3aa7a62774646b8f88d0b4a49e62ff6c60cc..c7ff0db3acdc207684492fc08455a8111d4fa73c 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -382,9 +382,6 @@ sig
   val e_map  : pool -> (term -> term) -> term -> term
   val e_iter : pool -> (term -> unit) -> term -> unit
 
-  val f_map  : (int -> term -> term) -> int -> term -> term
-  val f_iter : (int -> term -> unit) -> int -> term -> unit
-
   val lc_map : (term -> term) -> term -> term
   val lc_iter : (term -> unit) -> term -> unit
 
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index c3df0e1d46e8797d09fe245f7d1dac7208033735..be689edb26fdd79ffb821691afa863c633ad2582 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2338,12 +2338,6 @@ struct
         e_bind q x (f (lc_open x e))
     | _ -> rebuild f e
 
-  let f_map f n e =
-    match e.repr with
-    | Bind(q,t,e) -> c_bind q t (f (succ n) e)
-    | Apply(a,xs) -> e_apply (f n a) (List.map (f n) xs)
-    | _ -> rebuild (f n) e
-
   let lc_map f e =
     match e.repr with
     | Apply(a,xs) -> e_apply (f a) (List.map f xs)
@@ -2359,11 +2353,6 @@ struct
         lc_iter f (lc_open x e)
     | _ -> lc_iter f e
 
-  let f_iter f n e =
-    match e.repr with
-    | Bind(_,_,e) -> f (succ n) e
-    | _ -> lc_iter (f n) e
-
   (* -------------------------------------------------------------------------- *)
   (* --- Sub-terms                                                          --- *)
   (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 02fb5bd932695b843df0a9557da408896b87f560..d567a02694dfdc0e833f7eef515b4097bd01ebbf 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -868,7 +868,7 @@ let is_cint_simplifier = object (self)
         t v domain
 
   method assume p =
-    let rec aux i t =
+    let rec aux t =
       match Lang.F.repr t with
       | _ when not (is_prop t) -> ()
       | Fun(g,[a]) ->
@@ -877,10 +877,10 @@ let is_cint_simplifier = object (self)
               self#narrow_dom a ubound
             with Not_found -> ()
           end
-      | And _ -> Lang.F.QED.f_iter aux i t
+      | And _ -> Lang.F.QED.lc_iter aux t
       | _ -> ()
     in
-    aux 0 (Lang.F.e_prop p)
+    aux (Lang.F.e_prop p)
 
   method target _ = ()
   method fixpoint = ()