diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 1d6bae3b1a6f61cb780ca60043263d3b6f05288d..dfc55d03fc7e818fb7c19b8d70727f41b7b60485 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2162,7 +2162,8 @@ struct
 
   (* Alpha-convert free-variables in xs with the top-most bound variables *)
   (* Only activate flag subset if lc.vars is a subset of xs *)
-  let lc_close_xs ?(subset = false) ?(reversed = false) xs (lc : lc_term) : lc_term =
+  (* Warning: ~reversed:false needs to compute the length of xs *)
+  let lc_close_xs ?(subset = false) ~reversed xs (lc : lc_term) : lc_term =
     let mu = cache () in
     begin
       if reversed then