diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index f117f234c125306bb71f8b7496e44aa90bb8a827..6620c41a9b3e5d528d53541dfeff6cc7f01a27ec 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -306,9 +306,10 @@ sig
   (** Bind the given variable if it appears free in the term,
       or return the term unchanged. *)
 
-  val e_open : ?pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool ->
+  val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool ->
     term -> (binder * var) list * term
-  (** Open all the specified binders *)
+  (** Open all the specified binders
+      The pool must contain all free variables of the term. *)
 
   val e_close : (binder * var) list -> term -> term
   (** Closes all specified binders *)
@@ -348,7 +349,7 @@ sig
     (** Must bind lc-closed terms, or raise Invalid_argument *)
 
     val add_filter : t -> (term -> bool) -> unit
-    (** Only modifies terms that {i not} pass the filter. *)
+    (** Only modifies terms that {i pass} the filter. *)
 
     val add_var : t -> var -> unit
     (** To the pool *)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index b477ebcf5762b9a06344fe4a490e3ea986074f5d..58b7ee820bfa69205a53a2afa6e396c8aad9ce89 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2302,12 +2302,9 @@ struct
   let e_exists = bind_xs Exists
   let e_lambda = bind_xs Lambda
 
-  let e_open ?pool ?(forall=true) ?(exists=true) ?(lambda=true) a =
+  let e_open ~pool ?(forall=true) ?(exists=true) ?(lambda=true) a =
     match a.repr with
     | Bind _ ->
-        let pool = match pool with Some p -> p | None ->
-          let p = POOL.create () in
-          Vars.iter (POOL.add p) a.vars ; p in
         let filter = function
           | Forall -> forall
           | Exists -> exists