diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index a9079819ed7e584f342faa4a7aff9129d5ffda47..b2de4a157e3f8cddbbba1fa90ee614cf3d556bad 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -175,8 +175,8 @@ sig
   module Var : Variable
 
   type term
-  type bind
-
+  type lc_term
+  (** Loosely closed terms. *)
 
   module Term : Symbol with type t = term
 
@@ -219,10 +219,11 @@ sig
 
   (** {3 Terms} *)
 
-  type 'a expression = (Field.t,ADT.t,Fun.t,var,bind,'a) term_repr
+  type 'a expression = (Field.t,ADT.t,Fun.t,var,lc_term,'a) term_repr
 
   type repr = term expression
-  type path = int list (** position of a subterm in a term. *)
+  type lc_repr = lc_term expression
+
   type record = (Field.t * term) list
 
   val decide   : term -> bool (** Return [true] if and only the term is [e_true]. Constant time. *)
@@ -243,8 +244,18 @@ sig
   val sort : term -> sort   (** Constant time *)
   val vars : term -> Vars.t (** Constant time *)
 
+  (** Path-positioning access
+
+      This part of the API is DEPRECATED
+  *)
+
+  type path = int list (** position of a subterm in a term. *)
+
   val subterm: term -> path -> term
+  [@@deprecated "Path-access might be unsafe in presence of binders"]
+
   val change_subterm: term -> path -> term -> term
+  [@@deprecated "Path-access might be unsafe in presence of binders"]
 
   (** {3 Basic constructors} *)
 
@@ -300,21 +311,35 @@ sig
   val sigma_add : sigma -> term Tmap.t -> unit
 
   val e_subst : ?sigma:sigma -> (term -> term) -> term -> term
+  [@@deprecated "Might be unsafe in presence of binders"]
+
   val e_subst_var : var -> term -> term -> term
+  [@@deprecated "Might be unsafe in presence of binders"]
 
   (** {3 Locally Nameless Representation} *)
 
-  val lc_bind : var -> term -> bind (** Close [x] as a new bound variable *)
-  val lc_open : var -> bind -> term (** Instantiate top bound variable *)
-  val lc_open_term : term -> bind -> term
+  val lc_bind : var -> term -> lc_term (** Close [x] as a new bound variable *)
+  [@@deprecated "Might be unsafe in presence of binders"]
+
+  val lc_open : var -> lc_term -> term (** Instantiate top bound variable *)
+  [@@deprecated "Might be unsafe in presence of binders"]
+
+  val lc_open_term : term -> lc_term -> term
+  [@@deprecated "Might be unsafe in presence of binders"]
+
+
   (** Instantiate top bound variable with the given term *)
   val lc_closed : term -> bool
   val lc_closed_at : int -> term -> bool
   val lc_vars : term -> Bvars.t
-  val lc_repr : bind -> term
 
-  val binders : term -> binder list
+  val lc_term : term -> lc_term
+  val lc_repr : lc_term -> term
+  [@@deprecated "Might be unsafe in presence of binders"]
+
   (** Returns the list of head binders *)
+  val binders : term -> binder list
+  [@@deprecated "Useless function"]
 
   (** {3 Recursion Scheme} *)
 
@@ -325,7 +350,10 @@ sig
   val f_iter : (int -> term -> unit) -> int -> term -> unit
 
   val lc_map : (term -> term) -> term -> term
+  [@@deprecated "Might be unsafe in presence of binders"]
+
   val lc_iter : (term -> unit) -> term -> unit
+  [@@deprecated "Might be unsafe in presence of binders"]
 
   (** {3 Partial Typing} *)
 
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 3f909e5b7b0042e96e4652606a4dae3627bc4203..6b74f90b8c059da7002c7ef92a35da8c97cffeb4 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -65,9 +65,10 @@ struct
   }
   and repr = (Field.t,ADT.t,Fun.t,var,term,term) term_repr
 
-  type bind = term
+  type lc_term = term
+  type lc_repr = repr
 
-  type 'a expression = (Field.t,ADT.t,Fun.t,var,bind,'a) term_repr
+  type 'a expression = (Field.t,ADT.t,Fun.t,var,lc_term,'a) term_repr
 
   (* ------------------------------------------------------------------------ *)
   (* ---  Term Set,Map and Vars                                           --- *)
@@ -759,7 +760,7 @@ struct
   let e_zint z = insert (Kint z)
   let e_real x = insert (Kreal x)
   let e_var x  = insert(Fvar x)
-  let e_bvar k t = insert(Bvar(k,t))
+  let c_bvar k t = insert(Bvar(k,t))
 
   let c_div x y = insert (Div(x,y))
   let c_mod x y = insert (Mod(x,y))
@@ -1942,7 +1943,7 @@ struct
   let lc_bind x e =
     let k = Bvars.order e.bind in
     let t = tau_of_var x in
-    lc_subst_var (sigma ()) x (e_bvar k t) e
+    lc_subst_var (sigma ()) x (c_bvar k t) e
 
   let e_subst_var x v e =
     lc_subst_var (sigma ()) x v e
@@ -1968,6 +1969,7 @@ struct
   let lc_closed_at n e = Bvars.closed_at n e.bind
   let lc_vars e = e.bind
   let lc_repr e = e
+  let lc_term e = e
 
   (* -------------------------------------------------------------------------- *)
   (* --- Binders                                                            --- *)
@@ -2130,7 +2132,7 @@ struct
     | Kint z -> e_zint z
     | Kreal r -> e_real r
     | Fvar x -> e_var x
-    | Bvar(k,t) -> e_bvar k t
+    | Bvar(k,t) -> c_bvar k t
     | Bind(q,t,e) -> c_bind q t e
     | Apply(a,xs) -> e_apply a xs
     | Times(k,e) -> e_times k e
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index ac7a8919053453092eab3ece478e1c4a66edc8e4..4369fcafbc286ee29a4389a43bacf193a62d7a39 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -25,7 +25,7 @@ open Lang
 module PartitionsQQ : sig
   val destructs_qq :
     Lang.F.pool ->
-    Qed.Logic.binder -> tau:Lang.F.QED.tau -> phi:Lang.F.QED.bind ->
+    Qed.Logic.binder -> tau:Lang.F.QED.tau -> phi:Lang.F.QED.lc_term ->
     Lang.F.Vars.t * Lang.F.QED.term
 
   val get : vars:Lang.F.Vars.t -> Lang.F.term list ->