diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 8b5a4b76a1d36a0ef53613bf6f396519129a0706..b240e421dcb6f03e145c868cc700632468134fa8 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -222,7 +222,6 @@ sig
   type 'a expression = (Field.t,ADT.t,Fun.t,var,lc_term,'a) term_repr
 
   type repr = term expression
-  type lc_repr = lc_term expression
 
   type record = (Field.t * term) list
 
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index a1798c378127a35ba93c8a3f37ec0cf02a272f47..083477bab3f54bf99787b71cb94d0c28e80f10b6 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -66,7 +66,6 @@ struct
   and repr = (Field.t,ADT.t,Fun.t,var,term,term) term_repr
 
   type lc_term = term
-  type lc_repr = repr
 
   type 'a expression = (Field.t,ADT.t,Fun.t,var,lc_term,'a) term_repr