diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli
index 263c43e16af4d329a7578bcb4d3890451ccd90be..a78c5b919096d068d016650c23cfdbca586f78bc 100644
--- a/src/plugins/wp/Cint.mli
+++ b/src/plugins/wp/Cint.mli
@@ -77,10 +77,10 @@ val f_bitwised : lfun list (** All except f_bit *)
 
 (** Simplifiers *)
 
-val is_cint_simplifier: Conditions.simplifier
+val is_cint_simplifier: simplifier
 (** Remove the [is_cint] in formulas that are
     redundant with other conditions. *)
 
-val mask_simplifier: Conditions.simplifier
+val mask_simplifier: simplifier
 
 val is_positive_or_null: term -> bool
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index aa3a1478d52da357018dc3b254a78f684a5f0fbf..1fac69012b52aeae87e0b8ee5df50b9315ac4c54 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -845,23 +845,6 @@ and letify_case sigma ~target ~export seq =
 (* --- External Simplifier                                                --- *)
 (* -------------------------------------------------------------------------- *)
 
-exception Contradiction
-
-class type simplifier =
-  object
-    method name : string
-    method copy : simplifier
-    method assume : F.pred -> unit
-    method target : F.pred -> unit
-    method fixpoint : unit
-    method infer : F.pred list
-
-    method simplify_exp : F.term -> F.term
-    method simplify_hyp : F.pred -> F.pred
-    method simplify_branch : F.pred -> F.pred
-    method simplify_goal : F.pred -> F.pred
-  end
-
 let simplify_exp solvers e =
   List.fold_left (fun e s -> s#simplify_exp e) e solvers
 let simplify_goal solvers p =
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index 46607fa5871173d89b7e1b914b7de19f670f60cb..7a5c2b853e04159878577d9fd5b6a21d531a78be 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -180,36 +180,10 @@ val bundle : bundle -> sequence
 
 (** {2 Simplifier} *)
 
-exception Contradiction
-
-class type simplifier =
-  object
-    method name : string
-    method copy : simplifier
-    method assume : F.pred -> unit
-    (** Assumes the hypothesis *)
-    method target : F.pred -> unit
-    (** Give the predicate that will be simplified later *)
-    method fixpoint : unit
-    (** Called after assuming hypothesis and knowing the goal *)
-    method infer : F.pred list
-    (** Add new hypotheses implied by the original hypothesis. *)
-
-    method simplify_exp : F.term -> F.term
-    (** Currently simplify an expression. *)
-    method simplify_hyp : F.pred -> F.pred
-    (** Currently simplify an hypothesis before assuming it. In any
-        case must return a weaker formula. *)
-    method simplify_branch : F.pred -> F.pred
-    (** Currently simplify a branch condition. In any case must return an
-        equivalent formula. *)
-    method simplify_goal : F.pred -> F.pred
-    (** Simplify the goal. In any case must return a stronger formula. *)
-  end
-
 val clean : sequent -> sequent
 val filter : sequent -> sequent
 val parasite : sequent -> sequent
 val simplify : ?solvers:simplifier list -> ?intros:int -> sequent -> sequent
 val pruning : ?solvers:simplifier list -> sequent -> sequent
+
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 8577ac6702ad80d543bdcdd3cd103aeee30db076..3051ed18a418894640df2e2d9e1f912d80a38a97 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -1000,3 +1000,24 @@ struct
 end
 
 (* -------------------------------------------------------------------------- *)
+(* --- Simplifier                                                         --- *)
+(* -------------------------------------------------------------------------- *)
+
+exception Contradiction
+
+class type simplifier =
+  object
+    method name : string
+    method copy : simplifier
+    method assume : F.pred -> unit
+    method target : F.pred -> unit
+    method fixpoint : unit
+    method infer : F.pred list
+
+    method simplify_exp : F.term -> F.term
+    method simplify_hyp : F.pred -> F.pred
+    method simplify_branch : F.pred -> F.pred
+    method simplify_goal : F.pred -> F.pred
+  end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 4644a22391f0473387a54a6fad9ed2871a6d5e0a..e594b3720e9bce4b72f90903addb6f8e64f71e80 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -552,4 +552,33 @@ sig
 
 end
 
+(** {2 Simplifiers} *)
+
+exception Contradiction
+
+class type simplifier =
+  object
+    method name : string
+    method copy : simplifier
+    method assume : F.pred -> unit
+    (** Assumes the hypothesis *)
+    method target : F.pred -> unit
+    (** Give the predicate that will be simplified later *)
+    method fixpoint : unit
+    (** Called after assuming hypothesis and knowing the goal *)
+    method infer : F.pred list
+    (** Add new hypotheses implied by the original hypothesis. *)
+
+    method simplify_exp : F.term -> F.term
+    (** Currently simplify an expression. *)
+    method simplify_hyp : F.pred -> F.pred
+    (** Currently simplify an hypothesis before assuming it. In any
+        case must return a weaker formula. *)
+    method simplify_branch : F.pred -> F.pred
+    (** Currently simplify a branch condition. In any case must return an
+        equivalent formula. *)
+    method simplify_goal : F.pred -> F.pred
+    (** Simplify the goal. In any case must return a stronger formula. *)
+  end
+
 (* -------------------------------------------------------------------------- *)